Compfiles/Iran1998P3.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Iranian Mathematical Olympiad 1998, problem 3

Let x₁, x₂, x₃, x₄ be positive real numbers such that

x₁ ⬝ x₂ ⬝ x₃ ⬝ x₄ = 1.

Prove that x₁³ + x₂³ + x₃³ + x₄³ ≥ max(x₁ + x₂ + x₃ + x₄, 1/x₁ + 1/x₂ + 1/x₃ + 1/x₄).

Imports (3)
Imported by 1 file
  1. lemma Iran1998P3.cube_root_cube line 34 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, Eq, HPow.hPow, Nat, HDiv.hDiv

    Proof uses: Eq.mpr, HMul.hMul, id, congrArg, Eq.symm, Real.rpow_mul, mul_div_cancel₀, three_ne_zero, Real.rpow_one

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. problem Iran1998P3.iran1998_p3 line 40 source

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

    Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Eq, Finset.prod, Finset.range, LE.le, Max.max, Finset.sum, HDiv.hDiv, HPow.hPow

    Proof uses: Eq.mpr, And, id, congrArg, propext, max_le_iff, And.intro, HMul.hMul, Real.geom_mean_le_arith_mean_weighted, Membership.mem, Finset, Mathlib.Meta.NormNum.isRat_le_true, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv and 188 more

    172 instances, coercions and auxiliary constants left out.

    Tactic trace: 98 steps

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