FormalConjectures/ErdosProblems/604.lean

GitHub source file

6 declarations, 5 contain sorry, 0 declared as axioms

1. def Erdos604.pinnedDistinctDistances The pinned distance function $f(n)$ line 64 source

   Source documentation

   The pinned distance function $f(n)$. For a set $A$ of $n$ points in $\mathbb{R}^2$, take the largest number of distinct distances from a point $x \in A$ to the other points of $A$. Then $f(n)$ is the least such value over all such sets $A$.

   The distance $d(x, x) = 0$ is not counted, as in distinctDistancesFrom. Every $n$ admits a set of $n$ points in $\mathbb{R}^2$, so the infimum is a minimum.

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

   Statement uses: Nat

   Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, And, Eq, Finset.card, Finset.sup, distinctDistancesFrom, ENNReal

   14 instances, coercions and auxiliary constants left out.

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

2. theorem Erdos604.erdos_604 Documented declaration: erdos_604 sorry line 76 source

   Source documentation

   Given $n$ distinct points $A\subset\mathbb{R}^2$, must there be a point $x\in A$ such that $$\#\{ d(x,y) : y \in A\} \gg n^{1-o(1)}?$$

   This is the pinned distance problem, a stronger form of Problem 89. Here $n^{1-o(1)}$ means: for every $\varepsilon > 0$ and all large $n$, the bound is at least $n^{1-\varepsilon}$. We do not count the distance $d(x, x) = 0$; this changes the count by one.

   depends on sorry what this means

   Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, HPow.hPow, HSub.hSub, Erdos604.pinnedDistinctDistances, Filter.atTop

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

   27 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_604 : answer(sorry) ↔
       ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop,
         (n : ℝ) ^ (1 - ε) ≤ (pinnedDistinctDistances n : ℝ) := by
   …

   Mentions: Erdos604.pinnedDistinctDistances

3. theorem Erdos604.erdos_604.variants.sqrt_log Given $n$ distinct points $A\subset\mathbb{R}^2$, must there be a point $x\in A$ such that $$\#\{ d(x,y) : y \in A\} \gg \frac{n}{\sqrt{\log n}}?$$ sorry line 86 source

   Source documentation

   Given $n$ distinct points $A\subset\mathbb{R}^2$, must there be a point $x\in A$ such that $$\#\{ d(x,y) : y \in A\} \gg \frac{n}{\sqrt{\log n}}?$$

   depends on sorry what this means

   Statement uses: Iff, True, Asymptotics.IsBigO, Nat, Real, Filter.atTop, HDiv.hDiv, Real.sqrt, Real.log, Erdos604.pinnedDistinctDistances

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

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_604.variants.sqrt_log : answer(sorry) ↔
       (fun n : ℕ => (n : ℝ) / (n : ℝ).log.sqrt) =O[atTop]
         (fun n => (pinnedDistinctDistances n : ℝ)) := by
   …

   Mentions: Erdos604.pinnedDistinctDistances

4. theorem Erdos604.erdos_604.variants.grid_upper_bound Documented declaration: grid_upper_bound sorry line 100 source

   Source documentation

   The integer grid shows that $\frac{n}{\sqrt{\log n}}$ would be best possible: there are sets of $n$ points in $\mathbb{R}^2$ in which every point has $O(\frac{n}{\sqrt{\log n}})$ distinct distances to the other points. This follows from the bound of Erdős [Er46] on the total number of distinct distances in the grid (see Erdős Problem 89), since the number of distances from one point is at most the total number of distances. For $n$ that is not a square, take $n$ points of the smallest square grid with at least $n$ points.

   depends on sorry what this means

   Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos604.pinnedDistinctDistances, HDiv.hDiv, Real.sqrt, Real.log

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

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_604.variants.grid_upper_bound :
       (fun n => (pinnedDistinctDistances n : ℝ)) =O[atTop]
         (fun n : ℕ => (n : ℝ) / (n : ℝ).log.sqrt) := by
   …

   Mentions: Erdos604.pinnedDistinctDistances

5. theorem Erdos604.erdos_604.variants.katz_tardos Katz and Tardos [KaTa04] proved that some point of $A$ has $\gg n^{c-o(1)}$ distinct distances to the other points of $A$, where $$c=\frac{48-14e}{55-16e}=0.864137\cdots.$$ sorry line 111 source

   Source documentation

   Katz and Tardos [KaTa04] proved that some point of $A$ has $\gg n^{c-o(1)}$ distinct distances to the other points of $A$, where $$c=\frac{48-14e}{55-16e}=0.864137\cdots.$$

   depends on sorry what this means

   Statement uses: Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, HPow.hPow, HSub.hSub, HDiv.hDiv, HMul.hMul, Real.exp, Erdos604.pinnedDistinctDistances, Filter.atTop

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

   44 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_604.variants.katz_tardos :
       ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop,
         (n : ℝ) ^ ((48 - 14 * Real.exp 1) / (55 - 16 * Real.exp 1) - ε) ≤
           (pinnedDistinctDistances n : ℝ) := by
   …

   Mentions: Erdos604.pinnedDistinctDistances

6. theorem Erdos604.erdos_604.variants.average Let $d(x)$ be the number of distinct distances from $x$ to the other points of $A$ sorry line 127 source

   Source documentation

   Let $d(x)$ be the number of distinct distances from $x$ to the other points of $A$. Erdős [Er75f] conjectured that $$\sum_{x\in A}d(x) \gg \frac{n^2}{\sqrt{\log n}}$$ for every set $A\subset\mathbb{R}^2$ of $n$ points.

   The sum is at most $n$ times the largest $d(x)$, so this conjecture implies a positive answer to Erdos604.erdos_604.variants.sqrt_log.

   depends on sorry what this means

   Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Finset, EuclideanSpace, Fin, Eq, Finset.card, LE.le, HDiv.hDiv, HMul.hMul, HPow.hPow, Real.sqrt, Real.log, Finset.sum, distinctDistancesFrom and 2 more

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

   54 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_604.variants.average :
       ∃ C : ℝ, 0 < C ∧ ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℝ², #A = n →
         C * (n : ℝ) ^ 2 / (n : ℝ).log.sqrt ≤ ((∑ x ∈ A, distinctDistancesFrom A x : ℕ) : ℝ) := by
   …

   Mentions: distinctDistancesFrom