Planar Falconer distance theorem

Possible paper match, with no recorded review

Let $E\subset\R^d$ be compact, $d\ge2$, and
$\dim_HE>S=d/2$. Either Lemma~\ref{prep:classical-plane} already
proves that its distance set has positive Lebesgue measure, or the
following construction is possible.

After a similarity there are compact separated sets $E_1,E_2\subset E$
and probabilities $\mu_i$ supported on them, each satisfying
\[
 \mu_i(B(x,u))\le C u^{S+\chi}
\]
for a fixed $\chi>0$. Their cross directions lie in a fixed
arbitrarily small spherical patch. For every sufficiently small fixed
$\omega>0$, there are decreasing Borel pair sets
$\Gamma_N\subset E_1\times E_2$ such that
\begin{enumerate}
\item $(\mu_1\otimes\mu_2)(\bigcap_N\Gamma_N)>0$;
\item $\Gamma_N$ is a disjoint union of at most $C2^{2d\omega N}$
products of spatial Borel sets;
\item for every $e>0$, there are $c(e)>0$, $C_e<\infty$ and
Borel $B_N\subset\Gamma_N$ with
$(\mu_1\otimes\mu_2)(B_N)\le C_e2^{-c(e)N}$, such that for
$G_N=\Gamma_N\setminus B_N$, all $2^{-N}\le u\le1$, and
all spherical caps $B(w,u)$,
\begin{align*}
 \mu_2\{y:(x,y)\in G_N,\ \pi_x(y)\in B(w,u)\}
     &\le2^{eN}u^S,\\
 \mu_1\{x:(x,y)\in G_N,\ \pi_y(x)\in B(w,u)\}
     &\le2^{eN}u^S.
\end{align*}
\end{enumerate}
The last bounds integrate the original opposite marginal, without
normalizing its individual fibers. The $B_N$ need not have a product
partition or be nested. All constants are independent of $N$, but
may depend on the fixed measures, $\omega$, and $e$.

Other possible paper matches, closest wording first

• Theorem 1.1 of The Falconer distance conjecture in all dimensions. Words of the Lean statement, its names split into words, that also appear in the theorem: dim and compact. Found in the paper’s title, which its main theorem states: distance.
• Theorem 4.1 of The Falconer distance conjecture in all dimensions. Words of the Lean statement, its names split into words, that also appear in the theorem: dist. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: case.
• Proposition 11.5 of The Falconer distance conjecture in all dimensions. Words of the Lean statement, its names split into words, that also appear in the theorem: distance.
• Proposition 11.3 of The Falconer distance conjecture in all dimensions. Words of the Lean statement, its names split into words, that also appear in the theorem: distance.
• Theorem 4.2 of The Falconer distance conjecture in all dimensions. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: planar.
• Proposition 7.4 of The Falconer distance conjecture in all dimensions. Words of the Lean statement, its names split into words, that also appear in the theorem: distance.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.