PublishedFurstenberg.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The published planar incidence input

Orponen–Shmerkin–Wang, Kaufman and Falconer estimates for radial projections and a continuum version of Beck's theorem, Geom. Funct. Anal. 34 (2024), Definitions 2.5–2.6 and Theorem 2.7 (arXiv:2209.00348), following Orponen–Shmerkin, Duke Math. J. 172 (2023), Theorem 1.3 and Remark 1.4.

The proposition below is the separated finite-set specialization in one bounded, nonvertical line chart needed by ang:planar-measures. Only 0 < b ≤ 1/2 and b < f < 1 are retained. The chart identifies a line with its slope and intercept. Equivalence with the published line metric and replacement of covering counts by cardinalities cost fixed constants; the epsilon and the small-scale threshold below are chosen after these constants, not identified with the published theorem's original epsilon.

This is an explicit proposition to be supplied as a hypothesis. It is not a global axiom, and no proof of this published theorem is claimed here.

def OAI.Falconer.FiniteSeparatedAt line 28
Source documentation
Points and line parameters both use the Euclidean metric in this chart.
```
def FiniteSeparatedAt (δ : ℝ) (P : Finset (Space 2)) : Prop :=
…
```
Mentions: OAI.Falconer.Space
def OAI.Falconer.NormalizedFiniteBallBound line 32
Source documentation
The normalization is by the cardinality of the entire finite set.
```
def NormalizedFiniteBallBound (δ s K : ℝ) (P : Finset (Space 2)) : Prop := by
…
```
Mentions: OAI.Falconer.Space
def OAI.Falconer.InBoundedLineChart line 37
def OAI.Falconer.TubeIncident line 42
Source documentation
A point lies in the closed Euclidean δ-neighborhood of the line with slope l 0 and intercept l 1.
```
def TubeIncident (δ : ℝ) (x l : Space 2) : Prop :=
…
```
Mentions: OAI.Falconer.Space
def OAI.Falconer.PublishedPlanarFurstenberg line 47
Source documentation
Exactly the range of the published planar Furstenberg estimate needed by the higher-dimensional slicing argument, in a bounded line chart.
```
def PublishedPlanarFurstenberg : Prop := by
…
```