Compfiles/Imo2023P4.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2023, Problem 4

Let x₁, x₂, ... x₂₀₂₃ be distinct positive real numbers. Define

aₙ := √((x₁ + x₂ + ... + xₙ)(1/x₁ + 1/x₂ + ... + 1/xₙ)).

Suppose that aₙ is an integer for all n ∈ {1,...,2023}. Prove that 3034 ≤ a₂₀₂₃.

Imports (2)
Imported by 1 file
  1. def Imo2023P4.a line 31 source

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

    Statement uses: Subtype, Nat, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Real

    Proof uses: Real.sqrt, HMul.hMul, Finset.sum, Finset.filter, LE.le, Finset.univ, HDiv.hDiv

    23 instances, coercions and auxiliary constants left out.

  2. def Imo2023P4.aa line 37 source

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

    Statement uses: Nat, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Real

    Proof uses: Real.sqrt, Finset.sum, Finset.filter, LE.le, Finset.univ, HDiv.hDiv

    30 instances, coercions and auxiliary constants left out.

  3. lemma Imo2023P4.cauchy_schwarz line 42 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, HPow.hPow, Nat, HAdd.hAdd, Real.sqrt, HMul.hMul

    Proof uses: Fin, Unit, Finset.sum, Finset.univ, Real.sum_mul_le_sqrt_mul_sqrt, add_nonneg, Real.sqrt_nonneg, Eq, Real.sq_sqrt, mul_nonneg, Eq.mpr, id, congrArg, Eq.symm, pow_le_pow_left₀, Eq.mp, Real.sqrt_mul, congr, Eq.trans, Finset.sum_congr and 4 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

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

  4. lemma Imo2023P4.lemma1 line 76 source

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

    Statement uses: Real, Ne, OfNat.ofNat, LT.lt, Nat, HAdd.hAdd, HDiv.hDiv

    Proof uses: HMul.hMul, Eq.mpr, inferInstance, CommGroupWithZero, HPow.hPow, GroupWithZero, id, Eq, Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, Eq.trans, congr_arg₂, rfl, Mathlib.Tactic.FieldSimp.NF.mul_eq_eval and 98 more

    119 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  5. theorem Imo2023P4.imo2023_p4_generalized line 84 source

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

    Statement uses: Nat, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Real, LT.lt, Function.Injective, Exists, Int, Eq, Imo2023P4.aa, LE.le, Subtype.mk

    Proof uses: Nat.recAux, Eq.mpr, Finset.sum, Finset.filter, Eq.trans, congrFun', congrArg, MulZeroClass.mul_zero, zero_add, Finset.univ, Inv.inv, id, Real.sqrt, congr, CharP.cast_eq_zero, HDiv.hDiv, Finset.sum_congr, Finset.filter_congr, Iff.of_eq, Subtype.mk.congr_simp and 190 more

    275 instances, coercions and auxiliary constants left out.

    Tactic trace: 245 steps (first 200 of 245)

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

  6. problem Imo2023P4.imo2023_p4 line 383 source

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

    Statement uses: Subtype, Nat, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Real, LT.lt, Function.Injective, Exists, Int, Eq, Imo2023P4.a, LE.le, Subtype.mk

    Proof uses: HAdd.hAdd, HMul.hMul, Imo2023P4.aa, Imo2023P4.imo2023_p4_generalized, Eq.mpr, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_natCast, Nat.cast_one

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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