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

10 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1994, Problem 4

xᵢ is an infinite sequence of positive reals such that for all n, x₁ + x₂ + ... + xₙ ≥ √n. Show that x₁² + x₂² + ... + xₙ² > (1 + 1/2 + 1/3 + ... + 1/n) / 4 for all n.

Imports (5)
Imported by 1 file
  1. def Usa1994P4.y The telescoping comparison sequence y i = √(i+1) - √i line 42 source

    Source documentation

    The telescoping comparison sequence y i = √(i+1) - √i.

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

    Statement uses: Nat, Real

    Proof uses: HSub.hSub, Real.sqrt, HAdd.hAdd, OfNat.ofNat

    8 instances, coercions and auxiliary constants left out.

    noncomputable def y (i : ℕ) : ℝ := Real.sqrt (i + 1) - Real.sqrt i
  2. lemma Usa1994P4.hden_pos line 44 source

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

    Statement uses: Nat, LT.lt, Real, OfNat.ofNat, HAdd.hAdd, Real.sqrt

    Proof uses: add_pos_of_pos_of_nonneg, Real.sqrt_pos_of_pos, Right.add_pos_of_nonneg_of_pos, inferInstance, Zero, PartialOrder, Nat.cast_nonneg', Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, Real.sqrt_nonneg

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. lemma Usa1994P4.hy_pos line 47 source

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

    Statement uses: Nat, LT.lt, Real, OfNat.ofNat, Usa1994P4.y

    Proof uses: Real.sqrt, HAdd.hAdd, Real.sqrt_lt_sqrt, Nat.cast_nonneg, lt_add_one, Iff.mpr, HSub.hSub, sub_pos

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. lemma Usa1994P4.hy_mul line 52 source

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

    Statement uses: Nat, Eq, Real, HMul.hMul, Usa1994P4.y, HAdd.hAdd, Real.sqrt, OfNat.ofNat

    Proof uses: HPow.hPow, Real.sq_sqrt, le_of_lt, Right.add_pos_of_nonneg_of_pos, Nat.cast_nonneg', Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, Nat.cast_nonneg, id, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, HSub.hSub, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg and 62 more

    77 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  5. lemma Usa1994P4.hy_inv line 58 source

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

    Statement uses: Nat, Eq, Real, Usa1994P4.y, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd, Real.sqrt

    Proof uses: Iff.mpr, HMul.hMul, eq_div_iff_mul_eq, LT.lt.ne', Usa1994P4.hden_pos, Usa1994P4.hy_mul

    30 instances, coercions and auxiliary constants left out.

  6. lemma Usa1994P4.hy_succ_le line 61 source

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

    Statement uses: Nat, LE.le, Real, Usa1994P4.y, HAdd.hAdd, OfNat.ofNat

    Proof uses: Eq.mpr, HDiv.hDiv, Real.sqrt, id, Eq, congrArg, Usa1994P4.hy_inv, congrFun', Eq.trans, Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HMul.hMul, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 58 more

    80 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  7. lemma Usa1994P4.sum_y line 72 source

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

    Statement uses: Nat, Eq, Real, Finset.sum, Finset.range, Usa1994P4.y, Real.sqrt

    Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrArg, CharP.cast_eq_zero, Real.sqrt_zero, eq_self, Eq.mpr, HAdd.hAdd, id, Finset.sum_range_succ, congrFun', Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HMul.hMul, HPow.hPow and 32 more

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  8. lemma Usa1994P4.one_div_four_lt line 82 source

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

    Statement uses: Nat, LT.lt, Real, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd, HPow.hPow, Usa1994P4.y

    Proof uses: Real.sqrt, HMul.hMul, Real.sqrt_lt_sqrt, Nat.cast_nonneg, lt_add_one, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr and 80 more

    123 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  9. lemma Usa1994P4.sum_sq_y_le Abel-summation comparison: the partial sums of x dominate those of y and y is decreasing, so ∑ i, (y i)^2 ≤ ∑ i, x i * y i line 103 source

    Source documentation

    Abel-summation comparison: the partial sums of x dominate those of y and y is decreasing, so ∑ i, (y i)^2 ≤ ∑ i, x i * y i.

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

    Statement uses: Nat, Real, LE.le, Real.sqrt, Finset.sum, Finset.range, HPow.hPow, Usa1994P4.y, OfNat.ofNat, HMul.hMul

    Proof uses: Nat.casesAuxOn, of_eq_true, Eq, HAdd.hAdd, HSMul.hSMul, HSub.hSub, Finset.sum_range_by_parts, mul_le_mul_of_nonneg_left, Eq.mp, congrFun', congrArg, Eq.trans, Nat.cast_add, Nat.cast_one, LT.lt.le, Usa1994P4.hy_pos, Finset.sum_le_sum, Membership.mem, Finset, mul_le_mul_of_nonpos_left and 69 more

    119 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

    lemma sum_sq_y_le (x : ℕ → ℝ) (h : ∀ n : ℕ, Real.sqrt (n : ℝ) ≤ ∑ i ∈ Finset.range n, x i)
    (n : ℕ) :
    ∑ i ∈ Finset.range n, (y i) ^ 2 ≤ ∑ i ∈ Finset.range n, x i * y i := by
…

    Mentions: h, Usa1994P4.y

  10. problem Usa1994P4.usa1994_p4 line 136 source

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

    Statement uses: Nat, Real, LT.lt, OfNat.ofNat, LE.le, Real.sqrt, Finset.sum, Finset.range, HDiv.hDiv, HAdd.hAdd, HPow.hPow

    Proof uses: Eq.mpr, id, Eq, congrArg, Finset.sum_div, Ne, Usa1994P4.y, Finset.sum_lt_sum_of_nonempty, Iff.mpr, Finset.Nonempty, Finset.nonempty_range_iff, Membership.mem, Finset, Usa1994P4.one_div_four_lt, Finset.sum_pos, pow_pos, Usa1994P4.hy_pos, HMul.hMul, Usa1994P4.sum_sq_y_le, Finset.sum_mul_sq_le_sq_mul_sq and 7 more

    95 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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