Falconer distance set problem

DefinitionEuclidean distance set#✓fully proved

For a set \(E \subseteq \mathbb{R}^d\), the distance set of \(E\) is \(\Delta(E) = \{\lvert x - y \rvert : x, y \in E\}\), the set of Euclidean distances between pairs of points of \(E\).

def distanceSet {d : ℕ} (E : Set (EuclideanSpace ℝ (Fin d))) : Set ℝ :=
  {r | ∃ x ∈ E, ∃ y ∈ E, dist x y = r}

Sources

Guth, Iosevich, Ou, and Wang, arXiv:1808.09346v1, introduction.

Used by 11

Used byDistance set of the empty set · Distance sets of compact sets are compact · Distance sets of compact sets are Borel · Distance set of a singleton · Distances are nonnegative · Statement of Falconer's distance set theorem · Statement of Falconer's measure-zero distance set examples · Zero-measure distance sets give lower bounds for the planar distance threshold · Planar Falconer threshold property · The planar distance threshold is itself a threshold · Two is an admissible planar threshold

DefinitionPlanar Falconer threshold property#✓fully proved

An element \(s \in [0, \infty]\) has the planar threshold property when every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension \(\dim_H E > s\) has a distance set \(\{|x - y| : x, y \in E\}\) of positive one-dimensional Lebesgue measure.

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

Sources

the planar Falconer threshold in optimization catalogue C34a.

Uses 1 · Used by 12

Statement usesEuclidean distance set

Used byAdmissible planar threshold · Statement of the Guth–Iosevich–Ou–Wang planar distance set theorem · Zero-measure distance sets give lower bounds for the planar distance threshold · Real form of admissible planar thresholds · The planar distance threshold is admissible · Thresholds up to two with the planar threshold property bound the planar distance threshold · The planar distance threshold as a real infimum · The planar threshold property is upward closed · The planar distance threshold is itself a threshold · Real form of the admissible threshold family · Two is an admissible planar threshold · Wolff's planar distance set condition, as a proposition

DefinitionAdmissible planar threshold#✓fully proved

An extended nonnegative real \(s\) is an admissible planar threshold when \(0 \le s \le 2\) and \(s\) has the planar threshold property: every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension \(\dim_H E > s\) has a distance set of positive one-dimensional Lebesgue measure.

def admissiblePlanarThreshold (s : ℝ≥0∞) : Prop :=
  s ∈ Set.Icc 0 2 ∧ planarThresholdProperty s

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

MathlibExt/Geometry/FalconerDistanceSet.lean:37

Sources

the defining infimum in optimization catalogue C34a.

Uses 1 · Used by 11

Statement usesPlanar Falconer threshold property

Used byAdmissible planar thresholds exist · The planar distance threshold is attained · Zero-measure distance sets give lower bounds for the planar distance threshold · Real form of admissible planar thresholds · Planar distance threshold · The planar distance threshold is admissible · Admissible thresholds bound the planar distance threshold · The planar distance threshold as a real infimum · The planar distance threshold is itself a threshold · Real form of the admissible threshold family · Two is an admissible planar threshold

DefinitionPlanar distance threshold#✓fully proved

The planar distance threshold is the infimum, taken in \([0, \infty]\), of the admissible planar thresholds, that is, of all \(s \in [0, 2]\) such that every compact subset \(E\) of the Euclidean plane \(\mathbb{R}^2\) with Hausdorff dimension greater than \(s\) has a distance set of positive Lebesgue measure.

noncomputable def planarDistanceThreshold : ℝ≥0∞ :=
  sInf {s | admissiblePlanarThreshold s}

Sources

optimization catalogue C34a. The finite ENNReal representation retains the source's order and measure; finiteness and the real roundtrip are proved below.

Uses 1 · Used by 15

Statement usesAdmissible planar threshold

TheoremDistances are nonnegative#✓fully proved

For every set \(E \subseteq \mathbb{R}^d\), the distance set of \(E\) is contained in \([0, \infty)\).

theorem distanceSet_subset_nonnegative {d : ℕ} (E : Set (EuclideanSpace ℝ (Fin d))) :
    distanceSet E ⊆ Set.Ici (0 : ℝ)

Uses 1

Statement usesEuclidean distance set

TheoremDistance set of the empty set#✓fully proved

For every \(d\), the distance set of the empty subset of \(\mathbb{R}^d\) is empty.

theorem distanceSet_empty (d : ℕ) : distanceSet (∅ : Set (EuclideanSpace ℝ (Fin d))) = ∅

Uses 1

Statement usesEuclidean distance set

TheoremDistance set of a singleton#✓fully proved

For every point \(x \in \mathbb{R}^d\), the distance set of \(\{x\}\) is \(\{0\}\).

theorem distanceSet_singleton {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) :
    distanceSet ({x} : Set (EuclideanSpace ℝ (Fin d))) = {0}

Uses 1

Statement usesEuclidean distance set

TheoremDistance sets of compact sets are compact#✓fully proved

If \(E \subseteq \mathbb{R}^d\) is compact, then the distance set of \(E\) is a compact subset of \(\mathbb{R}\).

theorem distanceSet_isCompact {d : ℕ} {E : Set (EuclideanSpace ℝ (Fin d))}
    (h : IsCompact E) : IsCompact (distanceSet E)

Uses 1 · Used by 1

Statement usesEuclidean distance set

Used byDistance sets of compact sets are Borel

TheoremDistance sets of compact sets are Borel#✓fully proved

If \(E \subseteq \mathbb{R}^d\) is compact, then the distance set of \(E\) is a Borel measurable subset of \(\mathbb{R}\).

theorem distanceSet_measurableSet {d : ℕ} {E : Set (EuclideanSpace ℝ (Fin d))}
    (h : IsCompact E) : MeasurableSet (distanceSet E)

Uses 2

Statement usesEuclidean distance set

Proof usesDistance sets of compact sets are compact

TheoremThe planar threshold property is upward closed#✓fully proved

Let \(s \le t\) be elements of \([0, \infty]\). If \(s\) has the planar threshold property, that is, every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension \(\dim_H E > s\) has a distance set of positive one-dimensional Lebesgue measure, then \(t\) has the planar threshold property.

theorem planarThresholdProperty_mono {s t : ℝ≥0∞} (hs : planarThresholdProperty s)
    (hst : s ≤ t) : planarThresholdProperty t

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

MathlibExt/Geometry/FalconerDistanceSet.lean:37

Uses 1

Statement usesPlanar Falconer threshold property

TheoremSubsets of the plane have Hausdorff dimension at most two#✓fully proved

Every subset \(E\) of the Euclidean plane \(\mathbb{R}^2\) satisfies \(\dim_H E \le 2\).

theorem dimH_plane_le_two (E : Set (EuclideanSpace ℝ (Fin 2))) : dimH E ≤ (2 : ℝ≥0∞)

Used by 1

Used byTwo is an admissible planar threshold

TheoremTwo is an admissible planar threshold#✓fully proved

The number \(2\) is an admissible planar threshold: \(2 \in [0, 2]\), and every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension \(\dim_H E > 2\) has a distance set of positive Lebesgue measure. This holds vacuously, since no subset of the plane has Hausdorff dimension greater than \(2\).

theorem two_admissiblePlanarThreshold : admissiblePlanarThreshold 2

Uses 4 · Used by 2

Statement usesAdmissible planar threshold

Proof usesSubsets of the plane have Hausdorff dimension at most two · Euclidean distance set · Planar Falconer threshold property

Used byAdmissible planar thresholds exist · The planar distance threshold is at most two

TheoremAdmissible planar thresholds exist#✓fully proved

There is an admissible planar threshold, that is, the set of admissible planar thresholds is nonempty.

theorem admissiblePlanarThresholds_nonempty : {s | admissiblePlanarThreshold s}.Nonempty

Uses 2

Statement usesAdmissible planar threshold

Proof usesTwo is an admissible planar threshold

TheoremAdmissible thresholds bound the planar distance threshold#✓fully proved

For every \(s \in [0, \infty]\) that is an admissible planar threshold, the planar distance threshold is at most \(s\).

theorem planarDistanceThreshold_le_of_admissible {s : ℝ≥0∞}
    (hs : admissiblePlanarThreshold s) : planarDistanceThreshold ≤ s

def admissiblePlanarThreshold (s : ℝ≥0∞) : Prop :=
  s ∈ Set.Icc 0 2 ∧ planarThresholdProperty s

MathlibExt/Geometry/FalconerDistanceSet.lean:44

noncomputable def planarDistanceThreshold : ℝ≥0∞ :=
  sInf {s | admissiblePlanarThreshold s}

MathlibExt/Geometry/FalconerDistanceSet.lean:51

Uses 2 · Used by 3

Statement usesAdmissible planar threshold · Planar distance threshold

Used byThe planar distance threshold is attained · Thresholds up to two with the planar threshold property bound the planar distance threshold · The planar distance threshold is at most two

TheoremThe planar distance threshold is at most two#✓fully proved

The planar distance threshold is at most \(2\).

theorem planarDistanceThreshold_le_two : planarDistanceThreshold ≤ 2

Uses 3 · Used by 2

Statement usesPlanar distance threshold

Proof usesAdmissible thresholds bound the planar distance threshold · Two is an admissible planar threshold

Used byThe planar distance threshold is admissible · The planar distance threshold is finite

TheoremThe planar distance threshold is finite#✓fully proved

The planar distance threshold, an element of \([0, \infty]\), is not \(\infty\).

theorem planarDistanceThreshold_ne_top : planarDistanceThreshold ≠ ⊤

Uses 2 · Used by 1

Statement usesPlanar distance threshold

Proof usesThe planar distance threshold is at most two

Used byReal round trip of the planar distance threshold

TheoremReal round trip of the planar distance threshold#✓fully proved

Let \(\tau \in [0, \infty]\) be the planar distance threshold and let \(\tau_{\mathbb{R}}\) be its value as a real number (with the convention that \(\infty\) goes to \(0\)). Viewing \(\tau_{\mathbb{R}}\) again as an element of \([0, \infty]\) gives back \(\tau\).

theorem planarDistanceThreshold_ofReal_toReal :
    ENNReal.ofReal planarDistanceThreshold.toReal = planarDistanceThreshold

Uses 2

Statement usesPlanar distance threshold

Proof usesThe planar distance threshold is finite

TheoremTrivial lower bound for the planar distance threshold#✓fully proved

The planar distance threshold is at least \(0\).

theorem trivialLowerBound : (0 : ℝ≥0∞) ≤ planarDistanceThreshold

Uses 1

Statement usesPlanar distance threshold

TheoremThresholds up to two with the planar threshold property bound the planar distance threshold#✓fully proved

Thresholds up to two with the planar threshold property bound the planar distance threshold. For every \(s \in [0, \infty]\) with \(s \le 2\) that has the planar threshold property, the planar distance threshold is at most \(s\).

theorem planarDistanceThreshold_le_of_property {s : ℝ≥0∞} (hs : s ≤ 2)
    (hproperty : planarThresholdProperty s) : planarDistanceThreshold ≤ s

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

MathlibExt/Geometry/FalconerDistanceSet.lean:37

noncomputable def planarDistanceThreshold : ℝ≥0∞ :=
  sInf {s | admissiblePlanarThreshold s}

MathlibExt/Geometry/FalconerDistanceSet.lean:51

Uses 3

Statement usesPlanar distance threshold · Planar Falconer threshold property

Proof usesAdmissible thresholds bound the planar distance threshold

TheoremZero-measure distance sets give lower bounds for the planar distance threshold#✓fully proved

Let \(t \in [0, \infty]\). If \(E\) is a compact subset of the Euclidean plane \(\mathbb{R}^2\) whose Hausdorff dimension \(\dim_H E\) satisfies \(t \le \dim_H E\) and whose distance set has Lebesgue measure zero, then \(t\) is at most the planar distance threshold.

theorem le_planarDistanceThreshold_of_zeroMeasureWitness {t : ℝ≥0∞}
    {E : Set (EuclideanSpace ℝ (Fin 2))} (hcompact : IsCompact E) (hdim : t ≤ dimH E)
    (hzero : volume (distanceSet E) = 0) : t ≤ planarDistanceThreshold

def distanceSet {d : ℕ} (E : Set (EuclideanSpace ℝ (Fin d))) : Set ℝ :=
  {r | ∃ x ∈ E, ∃ y ∈ E, dist x y = r}

MathlibExt/Geometry/FalconerDistanceSet.lean:31

noncomputable def planarDistanceThreshold : ℝ≥0∞ :=
  sInf {s | admissiblePlanarThreshold s}

MathlibExt/Geometry/FalconerDistanceSet.lean:51

Uses 4

Statement usesEuclidean distance set · Planar distance threshold

Proof usesAdmissible planar threshold · Planar Falconer threshold property

TheoremReal form of admissible planar thresholds#✓fully proved

For every real number \(s \ge 0\), \(s\) is an admissible planar threshold (as an element of \([0, \infty]\)) if and only if \(s \in [0, 2]\) and \(s\) has the planar threshold property.

theorem ofReal_admissiblePlanarThreshold_iff {s : ℝ} (hs : 0 ≤ s) :
    admissiblePlanarThreshold (ENNReal.ofReal s) ↔
      s ∈ Set.Icc (0 : ℝ) 2 ∧ planarThresholdProperty (ENNReal.ofReal s)

def admissiblePlanarThreshold (s : ℝ≥0∞) : Prop :=
  s ∈ Set.Icc 0 2 ∧ planarThresholdProperty s

MathlibExt/Geometry/FalconerDistanceSet.lean:44

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

MathlibExt/Geometry/FalconerDistanceSet.lean:37

Uses 2 · Used by 1

Statement usesAdmissible planar threshold · Planar Falconer threshold property

Used byReal form of the admissible threshold family

TheoremThe planar distance threshold is itself a threshold#✓fully proved

Let \(s_0 \in [0, \infty]\) be the planar distance threshold, the infimum of the admissible planar thresholds. Every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension \(\dim_H E > s_0\) has a distance set of positive one-dimensional Lebesgue measure.

theorem planarThresholdProperty_planarDistanceThreshold :
    planarThresholdProperty planarDistanceThreshold

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

MathlibExt/Geometry/FalconerDistanceSet.lean:37

noncomputable def planarDistanceThreshold : ℝ≥0∞ :=
  sInf {s | admissiblePlanarThreshold s}

MathlibExt/Geometry/FalconerDistanceSet.lean:51

Uses 4 · Used by 1

Statement usesPlanar distance threshold · Planar Falconer threshold property

Proof usesAdmissible planar threshold · Euclidean distance set

Used byThe planar distance threshold is admissible

TheoremThe planar distance threshold is admissible#✓fully proved

The planar distance threshold is an admissible planar threshold: it lies in \([0, 2]\) and has the planar threshold property.

theorem planarDistanceThreshold_admissible : admissiblePlanarThreshold planarDistanceThreshold

def admissiblePlanarThreshold (s : ℝ≥0∞) : Prop :=
  s ∈ Set.Icc 0 2 ∧ planarThresholdProperty s

MathlibExt/Geometry/FalconerDistanceSet.lean:44

noncomputable def planarDistanceThreshold : ℝ≥0∞ :=
  sInf {s | admissiblePlanarThreshold s}

MathlibExt/Geometry/FalconerDistanceSet.lean:51

Uses 5 · Used by 1

Statement usesAdmissible planar threshold · Planar distance threshold

Proof usesThe planar distance threshold is at most two · Planar Falconer threshold property · The planar distance threshold is itself a threshold

Used byThe planar distance threshold is attained

TheoremThe planar distance threshold is attained#✓fully proved

The planar distance threshold is the least admissible planar threshold: it is itself an admissible planar threshold, and it is at most every admissible planar threshold.

theorem isLeast_admissiblePlanarThresholds :
    IsLeast {s | admissiblePlanarThreshold s} planarDistanceThreshold

def admissiblePlanarThreshold (s : ℝ≥0∞) : Prop :=
  s ∈ Set.Icc 0 2 ∧ planarThresholdProperty s

MathlibExt/Geometry/FalconerDistanceSet.lean:44

noncomputable def planarDistanceThreshold : ℝ≥0∞ :=
  sInf {s | admissiblePlanarThreshold s}

MathlibExt/Geometry/FalconerDistanceSet.lean:51

Uses 4

Statement usesAdmissible planar threshold · Planar distance threshold

Proof usesThe planar distance threshold is admissible · Admissible thresholds bound the planar distance threshold

TheoremReal form of the admissible threshold family#✓fully proved

The set of real numbers \(r \in [0, 2]\) such that \(r\), viewed as an element of \([0, \infty]\), has the planar threshold property equals the image of the set of admissible planar thresholds under the map \([0, \infty] \to \mathbb{R}\) that is the identity on finite values and sends \(\infty\) to \(0\).

theorem realThresholdFamily_eq_toReal_image :
    {r : ℝ | r ∈ Set.Icc 0 2 ∧ planarThresholdProperty (ENNReal.ofReal r)} =
      ENNReal.toReal '' {s | admissiblePlanarThreshold s}

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

MathlibExt/Geometry/FalconerDistanceSet.lean:37

def admissiblePlanarThreshold (s : ℝ≥0∞) : Prop :=
  s ∈ Set.Icc 0 2 ∧ planarThresholdProperty s

MathlibExt/Geometry/FalconerDistanceSet.lean:44

Uses 3 · Used by 1

Statement usesAdmissible planar threshold · Planar Falconer threshold property

Proof usesReal form of admissible planar thresholds

Used byThe planar distance threshold as a real infimum

TheoremThe planar distance threshold as a real infimum#✓fully proved

The value of the planar distance threshold as a real number (with the convention that \(\infty\) goes to \(0\)) equals the infimum in \(\mathbb{R}\) of the set of real numbers \(r \in [0, 2]\) that, as elements of \([0, \infty]\), have the planar threshold property.

theorem planarDistanceThreshold_toReal_eq_real_sInf :
    planarDistanceThreshold.toReal =
      sInf {r : ℝ | r ∈ Set.Icc 0 2 ∧ planarThresholdProperty (ENNReal.ofReal r)}

noncomputable def planarDistanceThreshold : ℝ≥0∞ :=
  sInf {s | admissiblePlanarThreshold s}

MathlibExt/Geometry/FalconerDistanceSet.lean:51

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

MathlibExt/Geometry/FalconerDistanceSet.lean:37

Uses 4

Statement usesPlanar distance threshold · Planar Falconer threshold property

Proof usesAdmissible planar threshold · Real form of the admissible threshold family

DefinitionStatement of Falconer's distance set theorem#✓fully proved

This is the proposition that for every integer \(d \ge 2\) and every compact set \(E \subseteq \mathbb{R}^d\) whose Hausdorff dimension is strictly greater than \((d+1)/2\), the distance set \(\{\|x - y\| : x, y \in E\}\) has positive one-dimensional Lebesgue measure.

def falconer1985GeneralSufficiency : Prop :=
  ∀ d : ℕ, 2 ≤ d → ∀ E : Set (EuclideanSpace ℝ (Fin d)), IsCompact E →
    ((d : ℝ≥0∞) + 1) / 2 < dimH E → 0 < volume (FalconerDistanceSet.distanceSet E)

Sources

GIOW, arXiv:1808.09346v1, introduction line 76, reporting Falconer (1985).

Uses 1 · Used by 1

Statement usesEuclidean distance set

Used byFalconer's distance set theorem

DefinitionWolff's planar distance set condition, as a proposition#✓fully proved

The proposition that every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension greater than \(4/3\) has a distance set \(\{|x - y| : x, y \in E\}\) of positive Lebesgue measure.

def wolff1999PlanarSufficiency : Prop :=
  FalconerDistanceSet.planarThresholdProperty ((4 : ℝ≥0∞) / 3)

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

MathlibExt/Geometry/FalconerDistanceSet.lean:37

Sources

GIOW, arXiv:1808.09346v1, introduction line 78, reporting Wolff (1999).

Uses 1 · Used by 1

Statement usesPlanar Falconer threshold property

Used byWolff's planar distance set theorem

DefinitionStatement of the Guth–Iosevich–Ou–Wang planar distance set theorem#✓fully proved

This is the proposition that \(5/4\) has the planar threshold property: every compact set \(E \subseteq \mathbb{R}^2\) whose Hausdorff dimension is strictly greater than \(5/4\) has a distance set \(\{\|x - y\| : x, y \in E\}\) of positive one-dimensional Lebesgue measure.

def guthIosevichOuWang2018PlanarSufficiency : Prop :=
  FalconerDistanceSet.planarThresholdProperty ((5 : ℝ≥0∞) / 4)

def planarThresholdProperty (s : ℝ≥0∞) : Prop :=
  ∀ E : Set (EuclideanSpace ℝ (Fin 2)), IsCompact E →
    s < dimH E → 0 < volume (distanceSet E)

MathlibExt/Geometry/FalconerDistanceSet.lean:37

Sources

Guth, Iosevich, Ou, and Wang, arXiv:1808.09346v1, Theorem 1.1, lines 80-81.

Uses 1 · Used by 1

Statement usesPlanar Falconer threshold property

Used byGuth–Iosevich–Ou–Wang planar distance set theorem

DefinitionStatement of Falconer's measure-zero distance set examples#✓fully proved

This is the proposition that for every integer \(d \ge 2\) and every \(s\) with \(0 \le s \le d/2\), there is a compact set \(E \subseteq \mathbb{R}^d\) of Hausdorff dimension exactly \(s\) whose distance set \(\{\|x - y\| : x, y \in E\}\) has one-dimensional Lebesgue measure zero.

def falconer1985LatticeExamples : Prop :=
  ∀ d : ℕ, 2 ≤ d → ∀ s : ℝ≥0∞, s ≤ (d : ℝ≥0∞) / 2 →
    ∃ E : Set (EuclideanSpace ℝ (Fin d)), IsCompact E ∧
      dimH E = s ∧ volume (FalconerDistanceSet.distanceSet E) = 0

Sources

GIOW, arXiv:1808.09346v1, introduction line 76. Dimensions use actual Hausdorff dimension and distance sets use actual one-dimensional Lebesgue measure.

Uses 1 · Used by 1

Statement usesEuclidean distance set

Used byFalconer's measure-zero distance set examples

DefinitionStatement of the upper bound \(3/2\) for the planar distance threshold#✓fully proved

This is the proposition that the planar distance threshold, the infimum of all \(s \in [0, 2]\) such that every compact set \(E \subseteq \mathbb{R}^2\) of Hausdorff dimension strictly greater than \(s\) has a distance set \(\{\|x - y\| : x, y \in E\}\) of positive one-dimensional Lebesgue measure, is at most \(3/2\).

def upperBound_Falconer1985 : Prop :=
  FalconerDistanceSet.planarDistanceThreshold ≤ (3 : ℝ≥0∞) / 2

Sources

optimization catalogue C34a, Falconer (1985) upper row.

Uses 1 · Used by 1

Statement usesPlanar distance threshold

Used byFalconer's upper bound for the planar distance threshold

DefinitionThe Wolff bound, as a proposition#✓fully proved

The proposition that the planar Falconer distance threshold is at most \(4/3\). Here the planar Falconer distance threshold is the infimum of the \(s \in [0, 2]\) such that every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension greater than \(s\) has a distance set \(\{|x - y| : x, y \in E\}\) of positive Lebesgue measure.

def upperBound_Wolff1999 : Prop :=
  FalconerDistanceSet.planarDistanceThreshold ≤ (4 : ℝ≥0∞) / 3

Sources

optimization catalogue C34a, Wolff (1999) upper row.

Uses 1 · Used by 1

Statement usesPlanar distance threshold

Used byWolff's upper bound for the planar Falconer threshold

DefinitionThe Guth–Iosevich–Ou–Wang bound, as a proposition#✓fully proved

The proposition that the planar Falconer distance threshold is at most \(5/4\). Here the planar Falconer distance threshold is the infimum of the \(s \in [0, 2]\) such that every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension greater than \(s\) has a distance set \(\{|x - y| : x, y \in E\}\) of positive Lebesgue measure.

def upperBound_GIOW2018 : Prop :=
  FalconerDistanceSet.planarDistanceThreshold ≤ (5 : ℝ≥0∞) / 4

Sources

optimization catalogue C34a, GIOW (2018) upper row.

Uses 1 · Used by 1

Statement usesPlanar distance threshold

Used byGuth–Iosevich–Ou–Wang upper bound for the planar Falconer threshold

DefinitionStatement of the lower bound \(1\) for the planar distance threshold#✓fully proved

This is the proposition that the planar distance threshold, the infimum of all \(s \in [0, 2]\) such that every compact set \(E \subseteq \mathbb{R}^2\) of Hausdorff dimension strictly greater than \(s\) has a distance set \(\{\|x - y\| : x, y \in E\}\) of positive one-dimensional Lebesgue measure, is at least \(1\).

def lowerBound_Falconer1985 : Prop :=
  (1 : ℝ≥0∞) ≤ FalconerDistanceSet.planarDistanceThreshold

Sources

optimization catalogue C34a and GIOW's endpoint lattice examples, line 76.

Uses 1 · Used by 1

Statement usesPlanar distance threshold

Used byFalconer's lower bound for the planar distance threshold

TheoremFalconer's distance set theorem#●ready to prove

For every integer \(d \ge 2\) and every compact set \(E \subseteq \mathbb{R}^d\) whose Hausdorff dimension is strictly greater than \((d+1)/2\), the distance set \(\{\|x - y\| : x, y \in E\}\) has positive one-dimensional Lebesgue measure.

theorem_wanted falconer1985GeneralSufficiency_holds : falconer1985GeneralSufficiency

def falconer1985GeneralSufficiency : Prop :=
  ∀ d : ℕ, 2 ≤ d → ∀ E : Set (EuclideanSpace ℝ (Fin d)), IsCompact E →
    ((d : ℝ≥0∞) + 1) / 2 < dimH E → 0 < volume (FalconerDistanceSet.distanceSet E)

WantedExt/Geometry/FalconerDistanceSetWanted.lean:33

Sources

GIOW, arXiv:1808.09346v1, line 76, reporting Falconer (1985).

Uses 1

Statement usesStatement of Falconer's distance set theorem

TheoremWolff's planar distance set theorem#●ready to prove

Every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension greater than \(4/3\) has a distance set \(\{|x - y| : x, y \in E\}\) of positive Lebesgue measure.

theorem_wanted wolff1999PlanarSufficiency_holds : wolff1999PlanarSufficiency

Sources

GIOW, arXiv:1808.09346v1, line 78, reporting Wolff (1999).

Uses 1

Statement usesWolff's planar distance set condition, as a proposition

TheoremGuth–Iosevich–Ou–Wang planar distance set theorem#●ready to prove

Every compact set \(E \subseteq \mathbb{R}^2\) whose Hausdorff dimension is strictly greater than \(5/4\) has a distance set \(\{\|x - y\| : x, y \in E\}\) of positive one-dimensional Lebesgue measure.

theorem_wanted guthIosevichOuWang2018PlanarSufficiency_holds :
  guthIosevichOuWang2018PlanarSufficiency

Sources

GIOW, arXiv:1808.09346v1, Theorem 1.1, lines 80-81.

Uses 1

Statement usesStatement of the Guth–Iosevich–Ou–Wang planar distance set theorem

TheoremFalconer's measure-zero distance set examples#●ready to prove

For every integer \(d \ge 2\) and every \(s\) with \(0 \le s \le d/2\), there is a compact set \(E \subseteq \mathbb{R}^d\) of Hausdorff dimension exactly \(s\) whose distance set \(\{\|x - y\| : x, y \in E\}\) has one-dimensional Lebesgue measure zero.

theorem_wanted falconer1985LatticeExamples_holds : falconer1985LatticeExamples

def falconer1985LatticeExamples : Prop :=
  ∀ d : ℕ, 2 ≤ d → ∀ s : ℝ≥0∞, s ≤ (d : ℝ≥0∞) / 2 →
    ∃ E : Set (EuclideanSpace ℝ (Fin d)), IsCompact E ∧
      dimH E = s ∧ volume (FalconerDistanceSet.distanceSet E) = 0

WantedExt/Geometry/FalconerDistanceSetWanted.lean:53

Sources

GIOW, arXiv:1808.09346v1, endpoint-inclusive lattice report, line 76.

Uses 1

Statement usesStatement of Falconer's measure-zero distance set examples

TheoremFalconer's upper bound for the planar distance threshold#●ready to prove

The planar distance threshold, the infimum of all \(s \in [0, 2]\) such that every compact set \(E \subseteq \mathbb{R}^2\) of Hausdorff dimension strictly greater than \(s\) has a distance set \(\{\|x - y\| : x, y \in E\}\) of positive one-dimensional Lebesgue measure, is at most \(3/2\).

theorem_wanted upperBound_Falconer1985_holds : upperBound_Falconer1985

Sources

optimization catalogue C34a, Falconer (1985) upper row.

Uses 1

Statement usesStatement of the upper bound \(3/2\) for the planar distance threshold

TheoremWolff's upper bound for the planar Falconer threshold#●ready to prove

The planar Falconer distance threshold, the infimum of the \(s \in [0, 2]\) such that every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension greater than \(s\) has a distance set \(\{|x - y| : x, y \in E\}\) of positive Lebesgue measure, is at most \(4/3\).

theorem_wanted upperBound_Wolff1999_holds : upperBound_Wolff1999

Sources

optimization catalogue C34a, Wolff (1999) upper row.

Uses 1

Statement usesThe Wolff bound, as a proposition

TheoremGuth–Iosevich–Ou–Wang upper bound for the planar Falconer threshold#●ready to prove

The planar Falconer distance threshold, the infimum of the \(s \in [0, 2]\) such that every compact set \(E \subseteq \mathbb{R}^2\) with Hausdorff dimension greater than \(s\) has a distance set \(\{|x - y| : x, y \in E\}\) of positive Lebesgue measure, is at most \(5/4\).

theorem_wanted upperBound_GIOW2018_holds : upperBound_GIOW2018

Sources

optimization catalogue C34a, GIOW (2018) upper row.

Uses 1

Statement usesThe Guth–Iosevich–Ou–Wang bound, as a proposition

TheoremFalconer's lower bound for the planar distance threshold#●ready to prove

The planar distance threshold, the infimum of all \(s \in [0, 2]\) such that every compact set \(E \subseteq \mathbb{R}^2\) of Hausdorff dimension strictly greater than \(s\) has a distance set \(\{\|x - y\| : x, y \in E\}\) of positive one-dimensional Lebesgue measure, is at least \(1\).

theorem_wanted lowerBound_Falconer1985_holds : lowerBound_Falconer1985

Sources

optimization catalogue C34a and GIOW, arXiv:1808.09346v1, line 76.

Uses 1

Statement usesStatement of the lower bound \(1\) for the planar distance threshold

34 fully proved8 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.