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

3 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2009, Problem 4

For n ≥ 2, let a₁, a₂, ..., aₙ be positive real numbers such that

(a₁ + a₂ + ... + aₙ) (1/a₁ + 1/a₂ + ... + 1/aₙ) ≤ (n + 1/2)².

Prove that max(a₁, a₂, ..., aₙ) ≤ 4 min(a₁, a₂, ..., aₙ).

Imports (2)
Imported by 1 file
  1. lemma Usa2009P4.sum_mul_sum_inv_ge Cross-paired Cauchy–Schwarz: for any two distinct indices p and q, the product (∑ aᵢ)(∑ 1/aᵢ) is bounded below by (√(a p / a q) + √(a q / a p) + (n - 2))² line 36 source

    Source documentation

    Cross-paired Cauchy–Schwarz: for any two distinct indices p and q, the product (∑ aᵢ)(∑ 1/aᵢ) is bounded below by (√(a p / a q) + √(a q / a p) + (n - 2))².

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

    Statement uses: Nat, Fin, Real, LT.lt, OfNat.ofNat, Ne, LE.le, HPow.hPow, HAdd.hAdd, Real.sqrt, HDiv.hDiv, HSub.hSub, HMul.hMul, Finset.sum, Finset.univ, Inv.inv

    Proof uses: Membership.mem, Finset, Finset.erase, Iff.mpr, And, Finset.mem_erase, And.intro, Ne.symm, Finset.mem_univ, Finset.card, Exists, Finset.one_lt_card, Exists.intro, Eq.mp, Fintype.card, congrArg, Fintype.card_fin, Finset.card_univ, Eq, Equiv.Perm and 42 more

    134 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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

    lemma sum_mul_sum_inv_ge {n : ℕ} {a : Fin n → ℝ} (ha : ∀ i, 0 < a i)
    {p q : Fin n} (hpq : p ≠ q) :
    (√(a p / a q) + √(a q / a p) + ((n : ℝ) - 2)) ^ 2 ≤
      (∑ i, a i) * (∑ i, (a i)⁻¹) := by
…
  2. lemma Usa2009P4.entry_le_four_mul_entry Any entry is at most 4 times any other entry line 101 source

    Source documentation

    Any entry is at most 4 times any other entry.

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

    Statement uses: Nat, Fin, Real, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, Finset.sum, Finset.univ, HDiv.hDiv, HPow.hPow, HAdd.hAdd

    Proof uses: Or, le_or_gt, le_of_not_gt, 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.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, Eq, id and 149 more

    158 instances, coercions and auxiliary constants left out.

    Tactic trace: 54 steps

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

    lemma entry_le_four_mul_entry {n : ℕ} {a : Fin n → ℝ} (ha : ∀ i, 0 < a i)
    (h : (∑ i, a i) * (∑ i, 1 / a i) ≤ ((n : ℝ) + 1 / 2) ^ 2) (p q : Fin n) :
    a p ≤ 4 * a q := by
…

    Mentions: h

  3. problem Usa2009P4.usa2009_p4 line 158 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Real, LT.lt, HMul.hMul, Finset.sum, Finset.univ, HDiv.hDiv, HPow.hPow, HAdd.hAdd, Finset.max', Finset.image, Iff.mpr, Finset.Nonempty, Finset.image_nonempty, Exists.intro, Membership.mem, Finset and 3 more

    Proof uses: And, Eq, Exists, Iff.mp, Finset.mem_image, Finset.max'_mem, Finset.min'_mem, Eq.mpr, id, congrArg, Eq.symm, Usa2009P4.entry_le_four_mul_entry

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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