Compfiles/Usa1978P1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1978, Problem 1

Given that a,b,c,d,e are real numbers such that

a + b + c + d + e = 8 a² + b² + c² + d² + e² = 16,

determine the maximum value of e.

Imports (2)
Imported by 1 file
  1. determine Usa1978P1.max_e line 30 source

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

    Statement uses: Real

    Proof uses: HDiv.hDiv, OfNat.ofNat

    7 instances, coercions and auxiliary constants left out.

  2. abbrev Usa1978P1.IsGood line 32 source

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

    Statement uses: Real

    Proof uses: And, Eq, HAdd.hAdd, OfNat.ofNat, HPow.hPow, Nat

    11 instances, coercions and auxiliary constants left out.

  3. problem Usa1978P1.usa1978_p1 line 35 source

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

    Statement uses: IsGreatest, Real, Set.ofPred, Exists, Usa1978P1.IsGood, Usa1978P1.max_e

    Proof uses: id, And, Membership.mem, Set, upperBounds, Eq, HAdd.hAdd, OfNat.ofNat, HPow.hPow, Nat, HDiv.hDiv, And.intro, LE.le, Exists.intro, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Meta.NormNum.IsNNRat.to_isNat, Mathlib.Meta.NormNum.isNNRat_add, Eq.refl, Mathlib.Meta.NormNum.isNNRat_div and 128 more

    120 instances, coercions and auxiliary constants left out.

    Tactic trace: 39 steps

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