Compfiles/Imo1999P2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1999, Problem 2

Let n ≥ 2 be a fixed integer. Find the least constant C such that

∑_{i < j} xᵢxⱼ(xᵢ² + xⱼ²) ≤ C (∑ i, xᵢ)⁴

for all non-negative real numbers x₁, ..., xₙ.

Imports (2)
Imported by 1 file
  1. determine Imo1999P2.C line 29 source

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

    Statement uses: Real

    Proof uses: HDiv.hDiv, OfNat.ofNat

    8 instances, coercions and auxiliary constants left out.

  2. problem Imo1999P2.imo1999_p2 line 31 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, IsLeast, Real, Set.ofPred, Fin, Finset.sum, Finset.univ, Finset.Ioi, HMul.hMul, HAdd.hAdd, HPow.hPow, Imo1999P2.C

    Proof uses: And.intro, Membership.mem, Set, lowerBounds, Finset.sum_nonneg, Finset, sq_nonneg, mul_nonneg, Eq, Finset.Iio, Eq.mpr, Sigma, Finset.sigma, Sigma.fst, Sigma.snd, id, congrArg, Finset.sum_sigma', Finset.sum_nbij', Sigma.mk and 177 more

    176 instances, coercions and auxiliary constants left out.

    Tactic trace: 133 steps

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