FormalConjectures/ErdosProblems/660.lean

GitHub source file

4 declarations, 3 contain sorry, 0 declared as axioms

1. def Erdos660.IsPolyhedronVertices Documented declaration: IsPolyhedronVertices line 43 source

   Source documentation

   P is the set of vertices of a (full-dimensional) convex polyhedron in $\mathbb{R}^3$: the points are in convex position and they affinely span $\mathbb{R}^3$ (so the polyhedron is genuinely three-dimensional).

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

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

   Proof uses: And, ConvexIndependent, Subtype, Membership.mem, Set, ENNReal, Eq, AffineSubspace, affineSpan, Top.top

   42 instances, coercions and auxiliary constants left out.

   def IsPolyhedronVertices (P : Finset ℝ³) : Prop :=
   …

2. theorem Erdos660.erdos_660 Let $x_1, \ldots, x_n \in \mathbb{R}^3$ be the vertices of a convex polyhedron sorry line 56 source

   Source documentation

   Let $x_1, \ldots, x_n \in \mathbb{R}^3$ be the vertices of a convex polyhedron. Are there at least $$(1 - o(1)) \frac{n}{2}$$ many distinct distances between the $x_i$?

   The $(1 - o(1)) \frac{n}{2}$ lower bound is formalised as: for every $\varepsilon > 0$, every set of $n$ vertices of a convex polyhedron with $n$ sufficiently large determines at least $(1 - \varepsilon) \frac{n}{2}$ distinct distances.

   depends on sorry what this means

   Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Finset, EuclideanSpace, Fin, Eq, Finset.card, Erdos660.IsPolyhedronVertices, LE.le, HMul.hMul, HSub.hSub, HDiv.hDiv, distinctDistances, ENNReal, Filter.atTop

   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_660 :
       answer(sorry) ↔
         ∀ ε : ℝ, 0 < ε → ∀ᶠ n in Filter.atTop, ∀ P : Finset ℝ³,
           P.card = n → IsPolyhedronVertices P →
           (1 - ε) * ((n : ℝ) / 2) ≤ (distinctDistances P : ℝ) := by
   …

   Mentions: Erdos660.IsPolyhedronVertices, distinctDistances

3. theorem Erdos660.erdos_660.variants.altman_planar For the similar problem in $\mathbb{R}^2$ there are always at least $n/2$ distances, as proved by Altman [Al63] sorry line 68 source

   Source documentation

   For the similar problem in $\mathbb{R}^2$ there are always at least $n/2$ distances, as proved by Altman [Al63].

   depends on sorry what this means

   Statement uses: Nat, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Eq, Finset.card, ConvexIndependent, Subtype, Membership.mem, Set, ENNReal, AffineSubspace, affineSpan, Top.top, LE.le, HDiv.hDiv, distinctDistances

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

   92 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_660.variants.altman_planar (n : ℕ) (P : Finset ℝ²)
       (hcard : P.card = n) (hconv : ConvexIndependent ℝ ((↑) : ↥(P : Set ℝ²) → ℝ²))
       (haff : affineSpan ℝ (P : Set ℝ²) = ⊤) :
       n / 2 ≤ distinctDistances P := by
   …

   Mentions: distinctDistances

4. theorem Erdos660.erdos_660.variants.Er75f In [Er75f] Erdős claims that Altman proved that the vertices determine $\gg n$ many distinct distances, but gives no reference sorry line 79 source

   Source documentation

   In [Er75f] Erdős claims that Altman proved that the vertices determine $\gg n$ many distinct distances, but gives no reference.

   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, Erdos660.IsPolyhedronVertices, LE.le, HMul.hMul, distinctDistances, ENNReal, Filter.atTop

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

   38 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_660.variants.Er75f :
       answer(sorry) ↔ ∃ c > (0 : ℝ), ∀ᶠ n in Filter.atTop, ∀ P : Finset ℝ³,
         P.card = n → IsPolyhedronVertices P →
         c * n ≤ (distinctDistances P : ℝ) := by
   …

   Mentions: c, Erdos660.IsPolyhedronVertices, distinctDistances