module
public import Mathlib.Tactic
public section
/-!
# International Mathematical Olympiad 1997, Problem 6
For each positive integer n, let f(n) denote the number of ways of representing n
as a sum of powers of 2 with non-negative integer exponents. Representations
which differ only in the ordering of their summands are considered to be the
same. For example, f(4) = 4, because 4 can be represented as 4, 2 + 2, 2 + 1 + 1
or 1 + 1 + 1 + 1. Prove that for any integer n ≥ 3,
2^(n²/4) < f(2^n) < 2^(n²/2).
-/
namespace Imo1997P6
/-- `f n` is the number of ways of representing `n` as a sum of powers of two
with non-negative integer exponents, where representations that differ only in
the order of their summands are considered the same. Rather than defining `f`
as a cardinality, we define it directly through its classical recurrence:
a representation of an odd number `2m + 1` must use a `1`, hence
`f (2m + 1) = f (2m)`; a representation of `2m + 2` either uses a `1` (and
deleting it gives a representation of `2m + 1`) or does not (and halving every
summand gives a representation of `m + 1`), hence
`f (2m + 2) = f (2m + 1) + f (m + 1)`. -/
def f : ℕ → ℕ
| 0 => 1
| n + 1 => f n + if (n + 1) % 2 = 0 then f ((n + 1) / 2) else 0
termination_by n => n
decreasing_by all_goals lia
theorem imo1997_p6 (n : ℕ) (hn : 3 ≤ n) :
(2 : ℝ) ^ ((n : ℝ) ^ 2 / 4) < (f (2 ^ n) : ℝ) ∧
(f (2 ^ n) : ℝ) < (2 : ℝ) ^ ((n : ℝ) ^ 2 / 2) := sorry
This problem has a complete formalized solution.