Compfiles/Imo1970P3.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

7 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1970, Problem 3

The real numbers a₀, a₁, a₂, ... satisfy 1 = a₀ ≤ a₁ ≤ a₂ ≤ ... . b₁, b₂, b₃, ... are defined by bₙ = ∑{k=1}^{n} (1 - a{k-1}/a_k)/√a_k.

(a) Prove that 0 ≤ bₙ < 2.

(b) Given c satisfying 0 ≤ c < 2, prove that we can find an so that bₙ > c for all sufficiently large n.

Imports (2)
Imported by 1 file
  1. structure Imo1970P3.IncreasingSequenceFromOne A sequence of real numbers satisfying the given conditions line 32 source

    Source documentation

    A sequence of real numbers satisfying the given conditions

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

    structure IncreasingSequenceFromOne where
…
  2. def Imo1970P3.b_seq The b_n sequence defined in terms of the a sequence line 38 source

    Source documentation

    The b_n sequence defined in terms of the a sequence

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

    Statement uses: Imo1970P3.IncreasingSequenceFromOne, Nat, Real

    Proof uses: Finset.sum, Finset.range, HDiv.hDiv, HSub.hSub, OfNat.ofNat, Imo1970P3.IncreasingSequenceFromOne.a, HAdd.hAdd, Real.sqrt

    11 instances, coercions and auxiliary constants left out.

    noncomputable def b_seq (seq : IncreasingSequenceFromOne) (n : ℕ) : ℝ :=
…

    Mentions: Imo1970P3.IncreasingSequenceFromOne

  3. def Imo1970P3.ValidBounds line 41 source

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

    Statement uses: Set, Real

    Proof uses: Set.ofPred, And, LE.le, OfNat.ofNat, LT.lt

    7 instances, coercions and auxiliary constants left out.

  4. def Imo1970P3.c_seq Helper: c_k = √(a_k) line 47 source

    Source documentation

    Helper: c_k = √(a_k)

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

    Statement uses: Imo1970P3.IncreasingSequenceFromOne, Nat, Real

    Proof uses: Real.sqrt, Imo1970P3.IncreasingSequenceFromOne.a

    noncomputable def c_seq (seq : IncreasingSequenceFromOne) (k : ℕ) : ℝ := Real.sqrt (seq.a k)

    Mentions: Imo1970P3.IncreasingSequenceFromOne

  5. lemma Imo1970P3.seq_pos All elements of the sequence are positive line 50 source

    Source documentation

    All elements of the sequence are positive

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

    Statement uses: Imo1970P3.IncreasingSequenceFromOne, Nat, LT.lt, Real, OfNat.ofNat, Imo1970P3.IncreasingSequenceFromOne.a

    Proof uses: Nat.recAux, Eq.mpr, id, Eq, congrArg, Imo1970P3.IncreasingSequenceFromOne.a_zero, zero_lt_one, LE.le, HAdd.hAdd, Imo1970P3.IncreasingSequenceFromOne.a_mono, Nat.le_succ, lt_of_lt_of_le

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

    lemma seq_pos (seq: IncreasingSequenceFromOne) : ∀ n, 0 < seq.a n := by
…

    Mentions: Imo1970P3.IncreasingSequenceFromOne

  6. lemma Imo1970P3.term_bound Key lemma: each term is bounded by 2(1/c_{k-1} - 1/c_k) line 61 source

    Source documentation

    Key lemma: each term is bounded by 2(1/c_{k-1} - 1/c_k)

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

    Statement uses: Imo1970P3.IncreasingSequenceFromOne, Nat, LE.le, Real, HDiv.hDiv, HSub.hSub, OfNat.ofNat, Imo1970P3.IncreasingSequenceFromOne.a, Real.sqrt, HMul.hMul, Imo1970P3.c_seq

    Proof uses: LT.lt, Iff.mpr, Real.sqrt_pos, Imo1970P3.seq_pos, Eq, HPow.hPow, of_eq_true, Eq.trans, True, congrArg, Real.sq_sqrt, le_of_lt, eq_self, Real.sqrt_le_sqrt, Imo1970P3.IncreasingSequenceFromOne.a_mono, Nat.sub_le, Eq.mpr, Inv.inv, id, congr and 148 more

    149 instances, coercions and auxiliary constants left out.

    Tactic trace: 35 steps

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

    lemma term_bound (seq : IncreasingSequenceFromOne) (k : ℕ) :
  (1 - seq.a (k - 1) / seq.a k) / Real.sqrt (seq.a k) ≤
  2 * (1 / c_seq seq (k - 1) - 1 / c_seq seq k) := by
…

    Mentions: Imo1970P3.IncreasingSequenceFromOne, Imo1970P3.c_seq

  7. problem Imo1970P3.imo1970_p3 line 113 source

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

    Statement uses: And, Imo1970P3.IncreasingSequenceFromOne, Nat, Membership.mem, Real, Set, Imo1970P3.ValidBounds, Imo1970P3.b_seq, Exists, GE.ge, LT.lt

    Proof uses: And.intro, LE.le, OfNat.ofNat, Finset.sum_nonneg, HDiv.hDiv, HSub.hSub, Imo1970P3.IncreasingSequenceFromOne.a, HAdd.hAdd, Real.sqrt, Finset.range, Finset, Imo1970P3.IncreasingSequenceFromOne.a_mono, Nat.le_succ, Imo1970P3.seq_pos, Iff.mpr, div_le_one, div_nonneg, sub_nonneg, Real.sqrt_nonneg, Nat.casesAuxOn and 271 more

    212 instances, coercions and auxiliary constants left out.

    Tactic trace: 145 steps

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