Compfiles/Usa2017P6.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2017, Problem 6

Find the minimum possible value of a / (b³ + 4) + b / (c³ + 4) + c / (d³ + 4) + d / (a³ + 4) given that a, b, c, d are nonnegative real numbers such that a + b + c + d = 4.

Imports (8)
Imported by 1 file
  1. def Usa2017P6.f line 32 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real

    Proof uses: Finset.sum, Finset.univ, HDiv.hDiv, HAdd.hAdd, HPow.hPow

    19 instances, coercions and auxiliary constants left out.

  2. def Usa2017P6.Conditions line 35 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real

    Proof uses: And, LE.le, Eq, Finset.sum, Finset.univ

    12 instances, coercions and auxiliary constants left out.

  3. lemma Usa2017P6.one_direction line 40 source

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

    Statement uses: Exists, Fin, OfNat.ofNat, Nat, Real, And, Usa2017P6.Conditions, Eq, Usa2017P6.f, HDiv.hDiv

    Proof uses: Exists.intro, Unit, Eq.mpr, LE.le, Finset.sum, Finset.univ, id, congrArg, Usa2017P6.Conditions.eq_1, HAdd.hAdd, HPow.hPow, Usa2017P6.f.eq_1, And.intro, propext, Pi.le_def, List, List.Mem, List.finRange, HEq, Membership.mem and 48 more

    87 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  4. lemma Usa2017P6.other_direction line 47 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Usa2017P6.Conditions, LE.le, HDiv.hDiv, Usa2017P6.f

    Proof uses: Eq, Finset.sum, Finset.univ, HSub.hSub, HAdd.hAdd, HPow.hPow, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, NNRat.rawCast, HMul.hMul, Nat.rawCast, Rat.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one and 129 more

    163 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

  5. determine Usa2017P6.solution line 71 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.

  6. problem Usa2017P6.usa2017_p6 line 73 source

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

    Statement uses: IsLeast, Real, Set.image, Fin, OfNat.ofNat, Nat, Usa2017P6.f, Set.ofPred, Usa2017P6.Conditions, Usa2017P6.solution

    Proof uses: And.intro, Membership.mem, Set, lowerBounds, of_eq_true, Eq.trans, Exists, And, Eq, True, id, Eq.mpr, LE.le, congrFun', congrArg, funext, forall_congr, implies_congr, Eq.refl, Usa2017P6.other_direction

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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