feat(ErdosProblems): 1088, Distinct Distances Conjecture in ℝᵈ#1386
Hidden character warning
feat(ErdosProblems): 1088, Distinct Distances Conjecture in ℝᵈ#1386manastole03 wants to merge 4 commits intogoogle-deepmind:mainfrom
Conversation
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
|
This PR adds Erdős Problem #1088, an open conjecture related to distinct distances among points in high-dimensional Euclidean space. The problem defines a function that measures the minimum number of points required so that any such set contains a subset of points where all pairwise distances are different. The conjecture asks for estimates of this function and whether it grows subexponentially with respect to the dimension when the number of points is fixed. Status: Open This contribution helps expand the repository’s coverage of open Erdős problems and makes this conjecture available for future discussion and exploration. |
YaelDillies
changed the title
YaelDillies
added
the
awaiting-author
|
@manastole03 are you still working on this? |
| variable {d : ℕ} | ||
|
|
||
| /-- A finite set of points has all pairwise distances distinct. -/ | ||
| def pairwiseDistancesDistinct (A : Finset (ℝ^d)) : Prop := |
There was a problem hiding this comment.
| def pairwiseDistancesDistinct (A : Finset (ℝ^d)) : Prop := | |
| def PairwiseDistancesDistinct (A : Finset (ℝ^d)) : Prop := |
same below
| ∀ d ≥ 3, ∃ c₁ c₂ : ℕ, 0 < c₁ ∧ c₁ ≤ c₂ ∧ | ||
| ∀ n ≥ 1, 2 ^ (c₁ * n) ≤ f d n ∧ f d n ≤ 2 ^ (c₂ * n) := by |
There was a problem hiding this comment.
f d n := 1.5 ^ n is definitely exponential but wouldn't be considered so by this definition.
| ∀ d ≥ 3, ∃ c₁ c₂ : ℕ, 0 < c₁ ∧ c₁ ≤ c₂ ∧ | |
| ∀ n ≥ 1, 2 ^ (c₁ * n) ≤ f d n ∧ f d n ≤ 2 ^ (c₂ * n) := by | |
| ∀ d ≥ 3, ∃ c₁ c₂ : \R, 0 < c₁ ∧ c₁ ≤ c₂ ∧ | |
| ∀ n ≥ 1, 2 ^ (c₁ * n) ≤ f d n ∧ f d n ≤ 2 ^ (c₂ * n) := by |
4 participants
This PR adds Erdős Problem #1088, an open conjecture related to distinct distances among points in high-dimensional Euclidean space.
The problem defines a function that measures the minimum number of points required so that any such set contains a subset of points where all pairwise distances are different. The conjecture asks for estimates of this function and whether it grows subexponentially with respect to the dimension when the number of points is fixed.
Status: Open
Reference: https://www.erdosproblems.com/1088
This contribution helps expand the repository’s coverage of open Erdős problems and makes this conjecture available for future discussion and exploration.
Closes #1288