FormalConjectures/ErdosProblems/655.lean

GitHub source file

3 declarations, 2 contain sorry, 0 declared as axioms

1. def Erdos655.IsValid A collection $x_1, \dots, x_n\in\mathbb{R}^2$ is valid if no circle whose centre is one of the $x_i$ contains three other points line 34 source

   Source documentation

   A collection $x_1, \dots, x_n\in\mathbb{R}^2$ is valid if no circle whose centre is one of the $x_i$ contains three other points.

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

   Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat

   Proof uses: Membership.mem, GT.gt, Not, LE.le, Set.ncard, Inter.inter, Set, Metric.sphere, ENNReal

   19 instances, coercions and auxiliary constants left out.

   def IsValid (X : Finset ℝ²) : Prop :=
   …

2. theorem Erdos655.erdos_655 Let $x_1,\ldots,x_n\in \mathbb{R}^2$ be such that no circle whose centre is one of the $x_i$ contains three other points sorry line 52 source

   Source documentation

   Let $x_1,\ldots,x_n\in \mathbb{R}^2$ be such that no circle whose centre is one of the $x_i$ contains three other points. Are there at least $$(1+c)\frac{n}{2}$$ distinct distances determined between the $x_i$, for some constant $c>0$ and all $n$ sufficiently large?

   The answer is no: as Zach Hunter observed, the regular n-gon (n points equally spaced on a circle) is valid and determines only ⌊n/2⌋ < (1+c)n/2 distinct distances, for every c > 0. (In the spirit of related conjectures of Erdős and others, presumably some kind of assumption that the points are in general position was intended; see erdos_655.variants.general_position.)

   The disproof — the regular n-gon construction together with its supporting lemmas — is formalised at the linked commit.

   depends on sorry what this means

   Statement uses: Iff, False, Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Finset, EuclideanSpace, Fin, Eq, Finset.card, Erdos655.IsValid, LE.le, HDiv.hDiv, HMul.hMul, HAdd.hAdd, distinctDistances and 2 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   56 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_655 :
       answer(False) ↔ ∃ c > (0 : ℝ), ∀ᶠ n in atTop, ∀ (X : Finset ℝ²), #X = n → IsValid X →
         (1 + c) * n / 2 ≤ distinctDistances X := by
   …

   Mentions: c, Erdos655.IsValid, distinctDistances

3. theorem Erdos655.erdos_655.variants.general_position Let $x_1,\ldots,x_n\in \mathbb{R}^2$ be such that no circle whose centre is one of the $x_i$ contains three other points sorry line 66 source

   Source documentation

   Let $x_1,\ldots,x_n\in \mathbb{R}^2$ be such that no circle whose centre is one of the $x_i$ contains three other points. Are there at least$$(1+c)\frac{n}{2}$$ distinct distances determined between the $x_i$, for some constant $c>0$ and all $n$ sufficiently large?

   In the spirit of related conjectures of Erdős and others, presumably some kind of assumption that the points are in general position (e.g. no three on a line and no four on a circle) was intended.

   depends on sorry what this means

   Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Finset, EuclideanSpace, Fin, Eq, Finset.card, Erdos655.IsValid, EuclideanGeometry.InGeneralPosition, LE.le, HDiv.hDiv, HMul.hMul, HAdd.hAdd and 3 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   60 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_655.variants.general_position :
       answer(sorry) ↔ ∃ c > (0 : ℝ), ∀ᶠ n in atTop, ∀ (X : Finset ℝ²), #X = n → IsValid X →
         InGeneralPosition X → (1 + c) * n / 2 ≤ distinctDistances X := by
   …

   Mentions: c, Erdos655.IsValid, distinctDistances