Compfiles/Imo1982P3.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

5 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1982, Problem 3

Consider infinite sequences $\{x_n \}$ of positive reals such that $x_0 = 0$ and $x_0 \geq x_1 \geq x_2 \geq ...$

a) Prove that for every such sequence there is an $n \geq 1$ such that:

$\frac{x_0^2}{x_1} + \ldots + \frac{x_{n-1}^2}{x_n} \geq 3.999$

b) Find such a sequence such that for all n:

$\frac{x_0^2}{x_1} + \ldots + \frac{x_{n-1}^2}{x_n} < 4$

Imports (3)
Imported by 1 file
  1. lemma Imo1982P3.le_avg x n is at most the average of all previous terms in the sequence line 50 source

    Source documentation

    x n is at most the average of all previous terms in the sequence. This is expressed here with ∑ k ∈ range n, x k added to both sides.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Ne, OfNat.ofNat, Antitone, LE.le, Finset.sum, Finset.range, HAdd.hAdd, HMul.hMul, HDiv.hDiv

    Proof uses: Eq.mpr, id, Eq, congrArg, Finset.sum_range_succ, mul_one_add, propext, add_le_add_iff_left, mul_one_div, le_div_iff₀, cast, LT.lt, Eq.symm, Eq.trans, congrFun', Nat.cast_zero, Ne.bot_lt, mul_comm, HSMul.hSMul, nsmul_eq_mul and 10 more

    109 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

    lemma le_avg {x : ℕ → ℝ} {n : ℕ} (hn : n ≠ 0) (hx : Antitone x) :
    ∑ k ∈ Finset.range (n + 1), x k ≤ (∑ k ∈ Finset.range n, x k) * (1 + 1 / n) := by
…
  2. lemma Imo1982P3.ineq The main inequality used for part a line 59 source

    Source documentation

    The main inequality used for part a.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Ne, OfNat.ofNat, Antitone, Eq, LT.lt, LE.le, HDiv.hDiv, HMul.hMul, HAdd.hAdd, Finset.sum, Finset.range, HPow.hPow

    Proof uses: Trans.trans, div_le_div_of_nonneg_right, mul_le_mul_of_nonneg_right, Eq.mpr, id, congrArg, propext, le_div_iff₀, Finset.sum_pos, Membership.mem, Finset, Iff.mpr, Finset.Nonempty, Finset.nonempty_range_iff, Eq.mp, congrFun', mul_one, four_mul_le_sq_add, le_of_lt, Nat.cast_pos' and 77 more

    152 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

    Open to load the checked before-and-after goal states.

    lemma ineq {x : ℕ → ℝ} {n : ℕ} (hn : n ≠ 0) (hx : Antitone x)
    (h0 : x 0 = 1) (hp : ∀ k, 0 < x k) :
    4 * n / (n + 1) ≤ ∑ k ∈ Finset.range (n + 1), x k ^ 2 / x (k + 1) := by
…
  3. problem Imo1982P3.imo1982_p3a line 87 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Antitone, Eq, OfNat.ofNat, LT.lt, Exists, LE.le, OfScientific.ofScientific, Bool.true, Finset.sum, Finset.range, HDiv.hDiv, HPow.hPow, HAdd.hAdd

    Proof uses: Exists.intro, Eq.mpr, HMul.hMul, Nat.succ, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm, Mathlib.Meta.NormNum.isNNRat_eq_true, Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true, Mathlib.Meta.NormNum.isNNRat_nnratCast, NNRat.divNat, Mathlib.Meta.NormNum.isNNRat_divNat, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1 and 15 more

    86 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  4. determine Imo1982P3.sol line 93 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real

    Proof uses: HPow.hPow, Inv.inv, OfNat.ofNat

    8 instances, coercions and auxiliary constants left out.

  5. problem Imo1982P3.imo1982_p3b line 95 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: And, Antitone, Nat, Real, Imo1982P3.sol, Eq, OfNat.ofNat, LT.lt, Finset.sum, Finset.range, HDiv.hDiv, HPow.hPow, HAdd.hAdd

    Proof uses: And.intro, StrictAnti.antitone, Inv.inv, pow_right_strictAnti₀, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_inv_pos, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, Nat.cast_one, pow_zero, of_eq_true, Eq.trans, True, forall_congr, congrArg and 67 more

    199 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

    Open to load the checked before-and-after goal states.