Documentation

IMOSLLean4.Main.IMO2023.A5.A5

IMO 2023 A5 #

Let $N > 0$ and $(a_0, a_1, …, a_N)$ be a permutation of $(0, 1, …, N)$. Suppose that $(|a_0 - a_1|, …, |a_{N - 1} - a_N|)$ is a permutation of $(1, 2, …, N)$. Prove that $\max\{a_0, a_N\} ≥ \lfloor (N + 1)/4 \rfloor + 1$.

Extra notes #

The lower bound is known to be sharp when $N \equiv 2 \pmod{4}$. We won't implement this at least until later when we figure out the other cases.

Extra lemmas #

source
theorem IMOSL.IMO2023A5.two_mul_add_dist_sq_eq (k m : ℕ) :
2 * k * m + k.dist m ^ 2 = k ^ 2 + m ^ 2
source
theorem IMOSL.IMO2023A5.add_sq_add_dist_sq_eq (k m : ℕ) :
(k + m) ^ 2 + k.dist m ^ 2 = 2 * (k ^ 2 + m ^ 2)
source
theorem IMOSL.IMO2023A5.succ_div_two_eq (N : ℕ) :
(N + 1) / 2 = N / 2 + N % 2
source
theorem IMOSL.IMO2023A5.div_two_add_succ_div_two (N : ℕ) :
N / 2 + (N + 1) / 2 = N
source
theorem IMOSL.IMO2023A5.two_mul_succ_div_two (N : ℕ) :
2 * ((N + 1) / 2) = N + N % 2
source
theorem IMOSL.IMO2023A5.mod_two_sq_eq_self (N : ℕ) :
(N % 2) ^ 2 = N % 2
source
theorem IMOSL.IMO2023A5.add_div_two_lt_max_of_ne {x y : ℕ} (h : x ≠ y) :
(x + y) / 2 < x.max y

Start of the problem #

source
structure IMOSL.IMO2023A5.nicePerm (N : ℕ) :
Type
Instances For
    source
    theorem IMOSL.IMO2023A5.nicePerm.sum_dist_abs_eq {N : ℕ} (X : nicePerm N) :
    2 * ∑ i : Fin N, (↑(X.toPerm i.castSucc)).dist ↑(X.toPerm i.succ) = (N + 1) * N
    source
    theorem IMOSL.IMO2023A5.nicePerm.sum_dist_rel_eq {N : ℕ} (X : nicePerm N) {k : ℕ} (hk : k ≤ N) :
    2 * ∑ i : Fin (N + 1), (↑(X.toPerm i)).dist k = (k + 1) * k + (N - k + 1) * (N - k)
    source
    theorem IMOSL.IMO2023A5.nicePerm.sum_dist_abs_le_sum_dist_rel {N : ℕ} (X : nicePerm N) (k : ℕ) :
    ∑ i : Fin N, (↑(X.toPerm i.castSucc)).dist ↑(X.toPerm i.succ) + ((↑(X.toPerm (Fin.last N))).dist k + (↑(X.toPerm 0)).dist k) ≤ 2 * ∑ i : Fin (N + 1), (↑(X.toPerm i)).dist k
    source
    theorem IMOSL.IMO2023A5.nicePerm.dist_rel_main_free_ineq {N : ℕ} (X : nicePerm N) {k : ℕ} (hk : k ≤ N) :
    2 * ((↑(X.toPerm (Fin.last N))).dist k + (↑(X.toPerm 0)).dist k) ≤ k.dist (N - k) ^ 2 + N
    source
    theorem IMOSL.IMO2023A5.nicePerm.toPerm_last_add_toPerm_zero_bound {N : ℕ} (X : nicePerm N) :
    (N + 1) / 2 ≤ ↑(X.toPerm (Fin.last N)) + ↑(X.toPerm 0)
    source
    theorem IMOSL.IMO2023A5.nicePerm.toPerm_last_max_toPerm_zero_bound {N : ℕ} (X : nicePerm N) :
    (if N = 0 then 0 else (N + 1) / 4 + 1) ≤ (↑(X.toPerm (Fin.last N))).max ↑(X.toPerm 0)
    source
    theorem IMOSL.IMO2023A5.final_solution {N : ℕ} (X : nicePerm N) :
    (if N = 0 then 0 else (N + 1) / 4 + 1) ≤ (↑(X.toPerm (Fin.last N))).max ↑(X.toPerm 0)

    Final solution