Documentation

IMOSLLean4.Main.IMO2006.N3

IMO 2006 N3 #

For each positive integer $n$, define $$ f(n) = \frac{1}{n} \sum_{k = 1}^n \left\lfloor \frac{n}{k} \right\rfloor. $$

  1. Prove that $f(n + 1) > f(n)$ infinitely often.
  2. Prove that $f(n + 1) < f(n)$ infinitely often.

Solution #

We follow the official solution. Throughout the code documentation, d denotes the divisor function.

source
def IMOSL.IMO2006N3.f (n : ℕ) :
ℚ

The function f(n) = 1/n ∑_{k ≤ n} ⌊n/k⌋.

Equations
Instances For
    source
    theorem IMOSL.IMO2006N3.sum_div_eq_sum_card_divisors (n : ℕ) :
    ∑ k ∈ Finset.Icc 1 n, n / k = ∑ k ∈ Finset.Icc 1 n, k.divisors.card

    The formula ∑_{k ≤ n} ⌊n/k⌋ = ∑_{k ≤ n} d(k).

    source
    theorem IMOSL.IMO2006N3.f_lt_f_of_sum_div {m n : ℕ} (h : m * ∑ k ∈ Finset.Icc 1 n, k.divisors.card < n * ∑ k ∈ Finset.Icc 1 m, k.divisors.card) :
    f n < f m

    If m ∑_{k ≤ n} d(k) < n ∑_{k ≤ m} d(k), then f(n) < f(m).

    Part 1 #

    source
    theorem IMOSL.IMO2006N3.exists_infinite_map_lt_of_lt_of_unbounded {g : ℕ → ℕ} (hg : ∀ (M : ℕ), ∃ (n : ℕ), M < g n) (N : ℕ) :
    ∃ n ≥ N, ∀ k < n, g k < g n

    Let g : ℕ → ℕ be an unbounded function. Then there exists infinitely many n such that g(k) < g(n) for all k < n.

    source
    theorem IMOSL.IMO2006N3.exists_infinite_card_divisors_lt_of_lt (N : ℕ) :
    ∃ n ≥ N, ∀ k < n, k.divisors.card < n.divisors.card

    There exists infinitely many n such that d(k) < d(n) for all k < n.

    source
    theorem IMOSL.IMO2006N3.f_pred_lt_of_card_divisors {n : ℕ} (hn : n > 0) (hn0 : ∀ k < n, k.divisors.card < n.divisors.card) :
    f (n - 1) < f n

    If n > 1 and d(k) < d(n) for all k < n, then f(n - 1) < f(n).

    source
    theorem IMOSL.IMO2006N3.final_solution_part1 (N : ℕ) :
    ∃ n ≥ N, f n < f (n + 1)

    Final solution, part 1

    Part 2 #

    source
    theorem IMOSL.IMO2006N3.one_lt_card_divisors {n : ℕ} (hn : n > 1) :
    n.divisors.card > 1

    For n > 1, we have d(n) > 1.

    source
    theorem IMOSL.IMO2006N3.two_mul_lt_sum_divisors {n : ℕ} (hn : n ≥ 6) :
    2 * n < ∑ k ∈ Finset.Icc 1 n, k.divisors.card

    For n ≥ 6, we have ∑_{k ≤ n} d(k) > 2n.

    source
    theorem IMOSL.IMO2006N3.f_lt_pred_of_prime {p : ℕ} (hp : p > 6) (hp0 : Nat.Prime p) :
    f p < f (p - 1)

    If p > 6 is prime, then f(p) < f(p - 1).

    source
    theorem IMOSL.IMO2006N3.final_solution_part2 (N : ℕ) :
    ∃ n ≥ N, f (n + 1) < f n

    Final solution, part 2