OP-00016 Open

Falconer's distance set conjecture

Let $d \ge 2$ and let $E \subset \mathbb{R}^d$ be a compact set of Hausdorff dimension greater than $d/2$. Then the distance set $\{\lvert x - y \rvert : x, y \in E\}$ has positive Lebesgue measure.

The hypothesis $d \ge 2$ is needed: $\mathbb{R}$ contains compact sets of dimension greater than $1/2$ whose distance set is null.

Source: Implicit in K. J. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212.

Classification

Primary: CA — Classical Analysis and ODEs
Secondary: MG
Keywords: distance sets, geometric measure theory, Hausdorff dimension

References

@article{falconer1985,
  author = {Falconer, K. J.},
  title = {On the {H}ausdorff dimensions of distance sets},
  journal = {Mathematika},
  volume = {32},
  pages = {206--212},
  year = {1985},
  doi = {10.1112/S0025579300010998}
}

@article{giow2020,
  author = {Guth, Larry and Iosevich, Alex and Ou, Yumeng and Wang, Hong},
  title = {On {F}alconer's distance set problem in the plane},
  journal = {Inventiones Mathematicae},
  volume = {219},
  pages = {779--830},
  year = {2020}
}

@misc{wikipedia,
  title = {Falconer's conjecture},
  howpublished = {Wikipedia},
  url = {https://en.wikipedia.org/wiki/Falconer%27s_conjecture}
}

@misc{formalconjectures,
  author = {{The Formal Conjectures Authors}},
  title = {Formal Conjectures},
  url = {https://github.com/google-deepmind/formal-conjectures/blob/0771383387505c96d1b2f6a3d35088ad00892c5c/FormalConjectures/Wikipedia/Falconer.lean#L43},
  note = {Lean statement under Apache-2.0; problem text under CC BY 4.0, or CC BY-SA 4.0 where it is based on Wikipedia}
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00016.

/-- OP-00016: Falconer's distance set conjecture -/
def Problem_OP_00016 : Prop :=
  ∀ (d : ℕ),
      2 ≤ d →
        ∀ (E : Set (EuclideanSpace ℝ (Fin d))),
          IsCompact E → ↑d < 2 * dimH E → 0 < MeasureTheory.volume (Set.image2 dist E E)

Formalised by The Formal Conjectures Authors (Apache-2.0); reviewed by clemens-admin.

Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.

Resolving this problem in Lean

Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.

In lakefile.toml:

[[require]]
name = "RegistryProblems"
git = "https://github.com/cthalhammer/registry-problems"
rev = "<published revision>"

In your proof:

import RegistryProblems.OP_00016

theorem resolution : RegistryProblems.Problem_OP_00016 := by
  sorry

In preprint.toml, mapping the claim to the declaration that establishes it:

[[statements]]
label = "Theorem 1"
lean = "resolution"
latex = "..."
problem = "OP-00016"
claim = "full"

To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:

theorem disproof : ¬ RegistryProblems.Problem_OP_00016 := by
  sorry

You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.

Citing this problem

This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.

OP-00016, "Falconer's distance set conjecture", clopen.solutions.