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

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1983, Problem 6

Suppose that a,b,c are the side lengths of a triangle. Prove that

a²b(a - b) + b²c(b - c) + c²a(c - a) ≥ 0.

Determine when equality occurs.

Imports (4)
Imported by 1 file
  1. lemma Imo1983P6.cauchy_schwarz_equals Equality in Cauchy-Schwarz implies linear dependence line 34 source

    Source documentation

    Equality in Cauchy-Schwarz implies linear dependence.

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

    Statement uses: Finset, Real, Exists, And, Membership.mem, Ne, OfNat.ofNat, Eq, HPow.hPow, Nat, Finset.sum, HMul.hMul

    Proof uses: HSub.hSub, HAdd.hAdd, Neg.neg, id, Eq.mpr, congrArg, Eq.trans, congrFun', congr, Finset.sum_mul, Finset.mul_sum, Finset.sum_congr, rfl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 79 more

    108 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

    lemma cauchy_schwarz_equals {ι: Type*} (s : Finset ι)
    (f g : ι → ℝ) (hf : ∃ i ∈ s, f i ≠ 0) :
    (∑ i ∈ s, f i * g i) ^ 2 = (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2 →
    ∃ r, ∀ i ∈ s, r * f i = g i := by
…

    Mentions: f

  2. theorem Imo1983P6.lemma1 line 70 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, Nat, And

    Proof uses: Fin, Matrix.vecCons, Real.sqrt, Matrix.vecEmpty, Exists, Membership.mem, Finset, Finset.univ, Imo1983P6.cauchy_schwarz_equals, Exists.intro, Ne, Eq.mpr, Not, id, Eq.trans, True, congr, congrArg, Or, true_and and 98 more

    118 instances, coercions and auxiliary constants left out.

    Tactic trace: 97 steps

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

  3. determine Imo1983P6.EqualityCondition line 147 source

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

    Statement uses: Real

    Proof uses: And, Eq

  4. problem Imo1983P6.imo1983_p6 line 149 source

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

    Statement uses: Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Dist.dist, Affine.Simplex.points, HAdd.hAdd, And, LE.le, HMul.hMul, HPow.hPow, HSub.hSub, Iff, Eq, Imo1983P6.EqualityCondition

    Proof uses: LT.lt, Not, Wbtw, AffineIndependent.not_wbtw_of_injective, of_decide_eq_true, Function.Injective, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, id, Bool, Decidable.decide, Bool.true, Eq.refl, Affine.Simplex.independent, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq and 159 more

    223 instances, coercions and auxiliary constants left out.

    Tactic trace: 75 steps

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