`Compfiles/Imo2021P2.lean`

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2021, Problem 2

Let n be a natural number, and let x₁, ..., xₙ be real numbers. Show that

∑ᵢ∑ⱼ √|xᵢ - xⱼ| ≤ ∑ᵢ∑ⱼ √|xᵢ + xⱼ|.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo2021P2.PiecewiseConcaveOn line 33 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real
Proof uses: LE.le, Membership.mem, Or, ConcaveOn, Set.Icc
9 instances, coercions and auxiliary constants left out.
lemma Imo2021P2.piecewise_concave_add line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, Imo2021P2.PiecewiseConcaveOn, Union.union, HAdd.hAdd
Proof uses: LE.le, Membership.mem, Or, ConcaveOn.add, Set.Icc, Finset.mem_union_left, Finset.mem_union_right
19 instances, coercions and auxiliary constants left out.
Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.piecewise_concave_sum line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Real, Membership.mem, Imo2021P2.PiecewiseConcaveOn, Finset.biUnion, Finset.sum
Proof uses: Finset.cons_induction, EmptyCollection.emptyCollection, Eq.mpr, OfNat.ofNat, id, Eq, congrArg, Finset.sum_empty, Finset.biUnion_empty, LE.le, Or, concaveOn_const, Set.Icc, Zero, convex_Icc, Not, Finset.cons, HAdd.hAdd, Finset.sum_cons, Insert.insert and 6 more
53 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
def Imo2021P2.UnboundedAtPosInfinity line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Exists, LE.le
1 instances, coercions and auxiliary constants left out.
lemma Imo2021P2.unbounded_at_pos_infinity_add line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Imo2021P2.UnboundedAtPosInfinity, HAdd.hAdd
Proof uses: LE.le, HDiv.hDiv, OfNat.ofNat, Nat, Exists, Exists.intro, Max.max, Eq.mpr, id, Eq, congrArg, Pi.add_apply, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 30 more
54 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.unbounded_at_pos_infinity_sum line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Finset.Nonempty, Real, Membership.mem, Imo2021P2.UnboundedAtPosInfinity, Finset.sum
Proof uses: Finset.Nonempty.cons_induction, Singleton.singleton, Eq.mpr, id, Eq, congrArg, Finset.sum_singleton, Finset.mem_singleton_self, Not, Finset.cons, HAdd.hAdd, Finset.sum_cons, Imo2021P2.unbounded_at_pos_infinity_add, Finset.mem_cons_self, Finset.mem_cons_of_mem
14 instances, coercions and auxiliary constants left out.
Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
def Imo2021P2.UnboundedAtNegInfinity line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Exists, LE.le
1 instances, coercions and auxiliary constants left out.
lemma Imo2021P2.unbounded_at_neg_infinity_add line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Imo2021P2.UnboundedAtNegInfinity, HAdd.hAdd
Proof uses: LE.le, HDiv.hDiv, OfNat.ofNat, Nat, Exists, Exists.intro, Min.min, Eq.mpr, id, Eq, congrArg, Pi.add_apply, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 30 more
54 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.unbounded_at_neg_infinity_sum line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Finset.Nonempty, Real, Membership.mem, Imo2021P2.UnboundedAtNegInfinity, Finset.sum
Proof uses: Finset.Nonempty.cons_induction, Singleton.singleton, Eq.mpr, id, Eq, congrArg, Finset.sum_singleton, Finset.mem_singleton_self, Not, Finset.cons, HAdd.hAdd, Finset.sum_cons, Imo2021P2.unbounded_at_neg_infinity_add, Finset.mem_cons_self, Finset.mem_cons_of_mem
14 instances, coercions and auxiliary constants left out.
Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
def Imo2021P2.PiecewiseConcavePlusOn line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real
Proof uses: And, Imo2021P2.PiecewiseConcaveOn, Imo2021P2.UnboundedAtPosInfinity, Imo2021P2.UnboundedAtNegInfinity
lemma Imo2021P2.piecewise_concave_plus_sum line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Finset.Nonempty, Real, Membership.mem, Imo2021P2.PiecewiseConcavePlusOn, Finset.biUnion, Finset.sum
Proof uses: Eq.mpr, And, Imo2021P2.PiecewiseConcaveOn, Imo2021P2.UnboundedAtPosInfinity, Imo2021P2.UnboundedAtNegInfinity, id, Eq, congrArg, Imo2021P2.PiecewiseConcavePlusOn.eq_1, And.intro, And.left, Imo2021P2.piecewise_concave_sum, And.right, Imo2021P2.unbounded_at_pos_infinity_sum, Imo2021P2.unbounded_at_neg_infinity_sum
10 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
def Imo2021P2.ExistsDecreaseOn line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real
Proof uses: Exists, And, Membership.mem, LE.le
3 instances, coercions and auxiliary constants left out.
lemma Imo2021P2.exists_decrease_of_piecewise_concave_plus line 160 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, Imo2021P2.PiecewiseConcavePlusOn, Imo2021P2.ExistsDecreaseOn
Proof uses: Imo2021P2.PiecewiseConcaveOn, And, Imo2021P2.UnboundedAtPosInfinity, Imo2021P2.UnboundedAtNegInfinity, WithBot, Finset.max, Finset.filter, LE.le, WithTop, Finset.min, dite, Exists, Membership.mem, Eq, Bot.bot, Top.top, False.elim, False, EmptyCollection.emptyCollection, Eq.mpr and 77 more
100 instances, coercions and auxiliary constants left out.
Tactic trace: 172 steps
Open to load the checked before-and-after goal states.
def Imo2021P2.Finset.SumSqrtDist line 308 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real
Proof uses: Finset.sum, Real.sqrt, abs, HSub.hSub
5 instances, coercions and auxiliary constants left out.
lemma Imo2021P2.piecewise_concave_sqrt_dist line 311 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Imo2021P2.PiecewiseConcaveOn, Singleton.singleton, Finset, Real.sqrt, abs, HSub.hSub
Proof uses: LE.le, Membership.mem, Or, Finset.mem_singleton_self, HPow.hPow, HDiv.hDiv, OfNat.ofNat, Nat, Eq, Function.comp, funext, id, Eq.mpr, congrArg, Real.sqrt_eq_rpow, Eq.refl, ConcaveOn, Set.Icc, Set, Set.image and 93 more
133 instances, coercions and auxiliary constants left out.
Tactic trace: 95 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.unbounded_at_pos_infinity_sqrt_dist line 393 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Imo2021P2.UnboundedAtPosInfinity, Real.sqrt, abs, HSub.hSub
Proof uses: Exists.intro, LE.le, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, id, Real.le_sqrt_of_sq_le, Eq.mpr, Eq, congrArg, abs_sub_comm, abs_of_nonneg, le_trans, sq_nonneg, Eq.mp, Eq.symm, propext, le_sub_iff_add_le'
48 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.unbounded_at_neg_infinity_sqrt_dist line 404 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Imo2021P2.UnboundedAtNegInfinity, Real.sqrt, abs, HSub.hSub
Proof uses: Exists.intro, LE.le, HPow.hPow, Nat, OfNat.ofNat, id, Real.le_sqrt_of_sq_le, Eq.mpr, Eq, congrArg, abs_of_nonneg, le_trans, sq_nonneg, Eq.mp, Eq.symm, propext, le_sub_comm
42 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.piecewise_concave_plus_sqrt_dist line 415 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Imo2021P2.PiecewiseConcavePlusOn, Singleton.singleton, Finset, Real.sqrt, abs, HSub.hSub
Proof uses: Eq.mpr, And, Imo2021P2.PiecewiseConcaveOn, Imo2021P2.UnboundedAtPosInfinity, Imo2021P2.UnboundedAtNegInfinity, id, Eq, congrArg, Imo2021P2.PiecewiseConcavePlusOn.eq_1, And.intro, Imo2021P2.piecewise_concave_sqrt_dist, Imo2021P2.unbounded_at_pos_infinity_sqrt_dist, Imo2021P2.unbounded_at_neg_infinity_sqrt_dist
10 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.piecewise_concave_plus_sum_sqrt_dist line 423 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Finset.Nonempty, Real, Imo2021P2.PiecewiseConcavePlusOn, Finset.image, Imo2021P2.Finset.SumSqrtDist
Proof uses: Membership.mem, Singleton.singleton, Real.sqrt, abs, HSub.hSub, Imo2021P2.piecewise_concave_plus_sqrt_dist, Finset.biUnion, Finset.sum, Imo2021P2.piecewise_concave_plus_sum, Eq, funext, Eq.mpr, id, congrArg, Imo2021P2.Finset.SumSqrtDist.eq_1, Finset.sum_apply, Eq.mp, Finset.biUnion_singleton
11 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.exists_decrease_sum_sqrt_dist line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Finset.Nonempty, Real, Imo2021P2.ExistsDecreaseOn, Finset.image, Imo2021P2.Finset.SumSqrtDist
Proof uses: Imo2021P2.exists_decrease_of_piecewise_concave_plus, Imo2021P2.piecewise_concave_plus_sum_sqrt_dist
2 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.exists_sum_sqrt_dist_le_sum_sqrt_dist line 440 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Finset.Nonempty, Real, Exists, And, Membership.mem, LE.le, Finset.sum, Real.sqrt, abs, HSub.hSub
Proof uses: Finset.image, Imo2021P2.Finset.SumSqrtDist, OfNat.ofNat, Imo2021P2.exists_decrease_sum_sqrt_dist, Eq, Eq.mp, congrArg, propext, Finset.mem_image, Exists.intro, Eq.mpr, id, and_iff_right, congr, Finset.sum_congr, Eq.refl, Eq.trans, HAdd.hAdd, HMul.hMul, HPow.hPow and 18 more
54 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2021P2.decrease_sum line 452 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Finset.Nonempty, Real, Exists, And, Membership.mem, LE.le, Finset.sum, Real.sqrt, abs, HSub.hSub, HAdd.hAdd
Proof uses: Prod, SProd.sprod, Imo2021P2.exists_sum_sqrt_dist_le_sum_sqrt_dist, Finset.Nonempty.product, Prod.mk, Exists.intro, Eq.mpr, id, Eq, congrArg, propext, and_iff_right, And.left, Eq.mp, And.intro, And.right, congr, Eq.trans, Prod.fst, Prod.snd and 3 more
27 instances, coercions and auxiliary constants left out.
Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Imo2021P2.imo2021_p2_finset_version line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Real, LE.le, Finset.sum, Real.sqrt, abs, HSub.hSub, HAdd.hAdd
Proof uses: Finset.strongInductionOn, LT.lt, dite, Not, Finset.Nonempty, Eq.mpr, EmptyCollection.emptyCollection, id, Eq, congrArg, Eq.mp, propext, Finset.not_nonempty_iff_eq_empty, OfNat.ofNat, Finset.sum_empty, le_refl, And, Membership.mem, Exists, Imo2021P2.decrease_sum and 111 more
115 instances, coercions and auxiliary constants left out.
Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
problem Imo2021P2.imo2021_p2 line 524 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, LE.le, Finset.sum, Finset.univ, Real.sqrt, abs, HSub.hSub, HAdd.hAdd
Proof uses: Imo2021P2.imo2021_p2_finset_version
11 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.