FormalConjectures/ErdosProblems/661.lean

GitHub source file

7 declarations, 5 contain sorry, 0 declared as axioms

1. def Erdos661.crossDistanceSet The set of distances $d(x, y)$ with $x \in A$ and $y \in B$ line 45 source

   Source documentation

   The set of distances $d(x, y)$ with $x \in A$ and $y \in B$.

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

   Statement uses: MetricSpace, Finset, Real

   Proof uses: Finset.image, Prod, Dist.dist, Prod.fst, Prod.snd, SProd.sprod

   4 instances, coercions and auxiliary constants left out.

   noncomputable def crossDistanceSet (A B : Finset X) : Finset ℝ :=
   …

2. def Erdos661.minimalCrossDistances The minimal number of distinct distances $d(x_i, y_j)$ over all choices of $2n$ distinct points $x_1, \ldots, x_n, y_1, \ldots, y_n$ in X line 54 source

   Source documentation

   The minimal number of distinct distances $d(x_i, y_j)$ over all choices of $2n$ distinct points $x_1, \ldots, x_n, y_1, \ldots, y_n$ in X.

   The $x_i$ form a set A of $n$ points, the $y_j$ form a set B of $n$ points, and A and B are disjoint, so all $2n$ points are distinct.

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

   Statement uses: MetricSpace, Nat

   Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, And, Eq, Finset.card, Disjoint, Real, Erdos661.crossDistanceSet

   3 instances, coercions and auxiliary constants left out.

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

3. theorem Erdos661.erdos_661 Are there, for all large sorry line 74 source

   Source documentation

   Are there, for all large $n$, some points $x_1,\ldots,x_n,y_1,\ldots,y_n\in \mathbb{R}^2$ such that the number of distinct distances $d(x_i,y_j)$ is $$o\left(\frac{n}{\sqrt{\log n}}\right)?$$

   We require all $2n$ points to be distinct; without any distinctness one could take all points equal and get a single distance. Writing $F(n)$ for the minimal number of such distances (minimalCrossDistances ℝ² n), the question asks whether $F(n) = o(n / \sqrt{\log n})$. This is equivalent to the existence, for all large $n$, of configurations whose count is at most $g(n)$ for some fixed $g(n) = o(n / \sqrt{\log n})$, since the infimum is attained.

   The source adds that one can also ask this for points in $\mathbb{R}^3$. Taken literally, the question is easy there, since a cubic grid of $2n$ points determines only $O(n^{2/3})$ distinct distances, so we do not state it.

   depends on sorry what this means

   Statement uses: Iff, True, Asymptotics.IsLittleO, Nat, Real, Filter.atTop, Erdos661.minimalCrossDistances, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, HDiv.hDiv, Real.sqrt, Real.log

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

   34 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_661 : answer(sorry) ↔
       (fun n => (minimalCrossDistances ℝ² n : ℝ)) =o[atTop]
         (fun (n : ℕ) => (n : ℝ) / (n : ℝ).log.sqrt) := by
   …

   Mentions: Erdos661.minimalCrossDistances

4. theorem Erdos661.erdos_661.variants.grid_upper_bound Take $2n$ points of the smallest square grid with at least $2n$ points; by [Er46] they determine $O(n / \sqrt{\log n})$ distinct distances sorry line 86 source

   Source documentation

   Take $2n$ points of the smallest square grid with at least $2n$ points; by [Er46] they determine $O(n / \sqrt{\log n})$ distinct distances. Splitting them into two halves of $n$ points shows that $F(n) = O(n / \sqrt{\log n})$. So the question is whether this trivial bound can be improved by more than a constant factor.

   depends on sorry what this means

   Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos661.minimalCrossDistances, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, HDiv.hDiv, Real.sqrt, Real.log

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

   34 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

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

   Mentions: Erdos661.minimalCrossDistances

5. theorem Erdos661.erdos_661.variants.le_minimalDistinctDistances Every split of a set of $2n$ points into two halves of $n$ points gives a configuration for $F(n)$, and the distances between the halves are among the distances of the whole set sorry line 98 source

   Source documentation

   Every split of a set of $2n$ points into two halves of $n$ points gives a configuration for $F(n)$, and the distances between the halves are among the distances of the whole set. Hence $F(n) \leq f(2n)$, where $f(2n)$ is the minimal number of distinct distances determined by $2n$ points in $\mathbb{R}^2$.

   depends on sorry what this means

   Statement uses: Nat, LE.le, Erdos661.minimalCrossDistances, EuclideanSpace, Real, Fin, OfNat.ofNat, ENNReal, minimalDistinctDistances, HMul.hMul

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

   26 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_661.variants.le_minimalDistinctDistances (n : ℕ) :
       minimalCrossDistances ℝ² n ≤ minimalDistinctDistances ℝ² (2 * n) := by
   …

   Mentions: Erdos661.minimalCrossDistances, minimalDistinctDistances

6. theorem Erdos661.erdos_661.variants.little_o_distinct_distances Documented declaration: little_o_distinct_distances sorry line 111 source

   Source documentation

   Let $F(2n)$ be the minimal number of distinct distances $d(x_i, y_j)$ for $2n$ distinct points $x_1,\ldots,x_n,y_1,\ldots,y_n\in \mathbb{R}^2$, and $f(2n)$ the minimal number of distinct distances determined by any $2n$ points in $\mathbb{R}^2$. Is $F = o(f)$?

   Here $F(2n)$ of erdosproblems.com is minimalCrossDistances ℝ² n (indexed by $n$ points on each side) and $f(2n)$ is minimalDistinctDistances ℝ² (2 * n). See also Erdős Problem 89.

   depends on sorry what this means

   Statement uses: Iff, True, Asymptotics.IsLittleO, Nat, Real, Filter.atTop, Erdos661.minimalCrossDistances, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, minimalDistinctDistances, HMul.hMul

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

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_661.variants.little_o_distinct_distances : answer(sorry) ↔
       (fun n => (minimalCrossDistances ℝ² n : ℝ)) =o[atTop]
         (fun n => (minimalDistinctDistances ℝ² (2 * n) : ℝ)) := by
   …

   Mentions: Erdos661.minimalCrossDistances, minimalDistinctDistances

7. theorem Erdos661.erdos_661.variants.lenz Documented declaration: lenz sorry line 124 source

   Source documentation

   In $\mathbb{R}^4$ Lenz observed (as stated on erdosproblems.com/661) that for every $n$ there are $2n$ distinct points $x_1,\ldots,x_n,y_1,\ldots,y_n\in \mathbb{R}^4$ with $d(x_i,y_j)=1$ for all $i,j$: take the $x_i$ on the circle of radius $1/\sqrt{2}$ about the origin in the plane of the first two coordinates, and the $y_j$ on the circle of radius $1/\sqrt{2}$ about the origin in the plane of the last two coordinates.

   depends on sorry what this means

   Statement uses: Nat, Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, And, Eq, Finset.card, Disjoint, Membership.mem, Dist.dist, ENNReal

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

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_661.variants.lenz (n : ℕ) :
       ∃ A B : Finset (EuclideanSpace ℝ (Fin 4)), #A = n ∧ #B = n ∧ Disjoint A B ∧
         ∀ x ∈ A, ∀ y ∈ B, dist x y = 1 := by
   …