FormalConjectures/ErdosProblems/756.lean

GitHub source file

5 declarations, 3 contain sorry, 0 declared as axioms

1. def Erdos756.richDistances The distances determined by A which occur for at least k many pairs of points of A line 43 source

   Source documentation

   The distances determined by A which occur for at least k many pairs of points of A.

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

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

   Proof uses: Finset.filter, LE.le, distanceMultiplicity, ENNReal, distanceSet

   13 instances, coercions and auxiliary constants left out.

   noncomputable def richDistances (A : Finset ℝ²) (k : ℕ) : Finset ℝ :=
   …

2. def Erdos756.maxRichDistances The largest number of distinct distances that a set of n points in $\mathbb{R}^2$ can determine, each of which occurs for more than n many pairs of points of the set line 48 source

   Source documentation

   The largest number of distinct distances that a set of n points in $\mathbb{R}^2$ can determine, each of which occurs for more than n many pairs of points of the set.

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

   Statement uses: Nat

   Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Eq, Finset.card, Erdos756.richDistances, HAdd.hAdd

   4 instances, coercions and auxiliary constants left out.

   noncomputable def maxRichDistances (n : ℕ) : ℕ :=
   …

3. theorem Erdos756.erdos_756 Let $A\subset \mathbb{R}^2$ be a set of $n$ points sorry line 59 source

   Source documentation

   Let $A\subset \mathbb{R}^2$ be a set of $n$ points. Can there be $\gg n$ many distinct distances each of which occurs for more than $n$ many pairs from $A$?

   The answer is yes: Bhowmick [Bh24] constructs a set of $n$ points in $\mathbb{R}^2$ such that $\lfloor\frac{n}{4}\rfloor$ distances occur at least $n+1$ times.

   depends on sorry what this means

   Statement uses: Iff, True, Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos756.maxRichDistances

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

   9 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_756 : answer(True) ↔
       (fun n : ℕ => (n : ℝ)) =O[atTop] (fun n : ℕ => (maxRichDistances n : ℝ)) := by
   …

   Mentions: Erdos756.maxRichDistances

4. theorem Erdos756.erdos_756.variants.bhowmick Bhowmick [Bh24] constructs a set of $n$ points in $\mathbb{R}^2$ such that $\lfloor\frac{n}{4}\rfloor$ distances occur at least $n+1$ times sorry line 68 source

   Source documentation

   Bhowmick [Bh24] constructs a set of $n$ points in $\mathbb{R}^2$ such that $\lfloor\frac{n}{4}\rfloor$ distances occur at least $n+1$ times.

   depends on sorry what this means

   Statement uses: Nat, Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, And, Eq, Finset.card, LE.le, HDiv.hDiv, Erdos756.richDistances, HAdd.hAdd

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

   12 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_756.variants.bhowmick (n : ℕ) :
       ∃ A : Finset ℝ², A.card = n ∧ n / 4 ≤ (richDistances A (n + 1)).card := by
   …

   Mentions: Erdos756.richDistances

5. theorem Erdos756.erdos_756.variants.bhowmick_general More generally, they construct, for any positive integer $m$ and large $n$, a set of $n$ points such that $\lfloor \frac{n}{2(m+1)}\rfloor$ distances occur at least $n+m$ times sorry line 78 source

   Source documentation

   More generally, they construct, for any positive integer $m$ and large $n$, a set of $n$ points such that $\lfloor \frac{n}{2(m+1)}\rfloor$ distances occur at least $n+m$ times.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, Filter.Eventually, Exists, Finset, EuclideanSpace, Real, Fin, And, Eq, Finset.card, HDiv.hDiv, HMul.hMul, HAdd.hAdd, Erdos756.richDistances, Filter.atTop

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

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_756.variants.bhowmick_general (m : ℕ) (hm : 1 ≤ m) :
       ∀ᶠ n : ℕ in atTop, ∃ A : Finset ℝ², A.card = n ∧
         n / (2 * (m + 1)) ≤ (richDistances A (n + m)).card := by
   …

   Mentions: Erdos756.richDistances