Compfiles/Imo2020P6.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2020, Problem 6

Consider an integer n > 1, and a set S of n points in the plane such that the distance between any two points in S is at least 1. Prove that there is a line l separating S such that the distance from any point of S to l is at least Ω(n ^ (-1/3)).

(A line l separates a set of points S if some segment jointing two points in S croses l.)

Imports (2)
Imported by 1 file
  1. theorem Imo2020P6.exists_between_and_separated line 42 source

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

    Statement uses: Finset, Real, Nat, LT.lt, Finset.card, Finset.filter, Membership.mem, Set, Set.Ioo, Exists, And, LE.le, HDiv.hDiv, HSub.hSub, HMul.hMul, OfNat.ofNat, abs

    Proof uses: Nat.casesAuxOn, Eq, False.elim, Nat.succ, Nat.le, HEq, False, Nat.le.refl, noConfusion_of_Nat, Nat.ctorIdx, Nat.le.step, Eq.refl, HEq.refl, Eq.symm, HAdd.hAdd, Eq.mpr, id, congrArg, rfl, Fin and 205 more

    284 instances, coercions and auxiliary constants left out.

    Tactic trace: 80 steps

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

  2. def Imo2020P6.project Computes "how far along" the segment from a to b the point p lies line 119 source

    Source documentation

    Computes "how far along" the segment from a to b the point p lies.

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

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor

    Proof uses: HDiv.hDiv, ContinuousLinearMap, RingHom.id, starRingEnd, innerSL, VSub.vsub, Norm.norm

    46 instances, coercions and auxiliary constants left out.

    noncomputable def project (a b p : P) : ℝ := innerSL ℝ (a -ᵥ b) (a -ᵥ p) / ‖a -ᵥ b‖

    Mentions: P

  3. theorem Imo2020P6.project_self_left line 121 source

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

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Eq, Imo2020P6.project, OfNat.ofNat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HDiv.hDiv, ContinuousLinearMap, RingHom.id, starRingEnd, innerSL, VSub.vsub, Norm.norm, vsub_self, inner_zero_right, zero_div, eq_self

    63 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. theorem Imo2020P6.project_self_right line 122 source

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

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Ne, Eq, Imo2020P6.project, Norm.norm, VSub.vsub

    Proof uses: id, Eq.mpr, HDiv.hDiv, Inner.inner, HPow.hPow, Nat, OfNat.ofNat, congrArg, real_inner_self_eq_norm_sq, HMul.hMul, propext, div_eq_iff, norm_ne_zero_iff, vsub_ne_zero, pow_two, Eq.refl

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  5. theorem Imo2020P6.exists_affine_between_and_separated line 128 source

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

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Nat, Fact, Eq, Module.finrank, HAdd.hAdd, OfNat.ofNat, Finset, LE.le, LT.lt, Dist.dist, Finset.card, Finset.filter, Membership.mem, Set, Set.Ioo and 13 more

    Proof uses: Nat.floor, abs, Imo2020P6.exists_between_and_separated, Eq.mpr, id, congrArg, Eq.symm, propext, Nat.cast_lt, Eq.trans, Nat.cast_add, Nat.cast_one, lt_imp_lt_of_le_of_le, le_refl, Nat.lt_floor_add_one, Exists.intro, AffineSubspace.mk', AffineMap, AffineMap.lineMap, LinearMap.ker and 143 more

    323 instances, coercions and auxiliary constants left out.

    Tactic trace: 55 steps

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

  6. theorem Imo2020P6.card_le_of_separated line 193 source

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

    Statement uses: Finset, Real, LT.lt, OfNat.ofNat, LE.le, Set.Pairwise, Dist.dist, Membership.mem, Set, Set.Icc, Int, Finset.card, Int.floor, HAdd.hAdd, HDiv.hDiv, HSub.hSub

    Proof uses: Nat, Finset.Icc, Finset.card_le_card_of_injOn, Eq.mpr, id, Eq, congrArg, Finset.coe_Icc, And, propext, Set.mem_Icc, And.intro, Int.floor_nonneg, div_nonneg, sub_nonneg, And.left, LT.lt.le, Int.floor_le_floor, div_le_div_iff_of_pos_right, sub_le_sub_iff_right and 68 more

    144 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

  7. theorem Imo2020P6.card_le_of_separated_in_strip In a strip of width 1/2, if the points have pairwise distance at least 1, then we can bound the number of points line 222 source

    Source documentation

    In a strip of width 1/2, if the points have pairwise distance at least 1, then we can bound the number of points.

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

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, AffineIsometryEquiv, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Finset, Set.Pairwise, Finset.filter, Membership.mem, Set, Set.Ioo, HDiv.hDiv, WithLp.ofLp, LE.le and 5 more

    Proof uses: Int, Int.floor, HAdd.hAdd, Neg.neg, Imo2020P6.card_le_of_separated, Mathlib.Meta.NormNum.isNNRat_lt_true, 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, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool, Bool.true, le_of_not_gt and 143 more

    235 instances, coercions and auxiliary constants left out.

    Tactic trace: 29 steps

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

    theorem card_le_of_separated_in_strip (eqv : P ≃ᵃⁱ[ℝ] EuclideanSpace ℝ (Fin 2)) (S : Finset P)
    (h_sep : (S.filter (eqv · 0 ∈ Set.Ioo 0 (1 / 2)) : Set P).Pairwise fun x y => 1 ≤ dist x y)
    {N : ℝ} (hN : 1 ≤ N) (h_bound : ∀ x ∈ S.filter (eqv · 0 ∈ Set.Ioo 0 (1 / 2)), |eqv x 1| ≤ N) :
    #(S.filter (eqv · 0 ∈ Set.Ioo 0 (1/2))) ≤ N*6-1 := by
…

    Mentions: P, S

  8. problem Imo2020P6.imo2020_p6 line 254 source

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

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, Exists, And, LT.lt, Finset, Finset.card, Set.Pairwise, LE.le, Dist.dist, AffineSubspace, Subtype and 9 more

    Proof uses: Exists.intro, And.intro, Mathlib.Meta.NormNum.isNNRat_lt_true, 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, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool, Bool.true, dite, lt_of_lt_of_le, Real.rpow_pos_of_pos, Iff.mpr and 308 more

    349 instances, coercions and auxiliary constants left out.

    Tactic trace: 117 steps

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