AllDimensions.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The all-dimensional Falconer statement and the final measure argument

The Falconer distance conjecture concerns compact subsets of Euclidean space with Hausdorff dimension greater than half the ambient dimension. The dimension-independent final measure argument reduces positivity of the original distance set to absolute continuity of a weighted distance pushforward.

abbrev OAI.Falconer.Space line 26
Also declared: OAI/MeasureTheory/FalconerCompletion/Measures/StartingPairCompletion.lean:112 (same declaration text).
def OAI.Falconer.distanceSet line 29
Source documentation
Original Euclidean distances; auxiliary projections are not used here.
Distinct definitions of this name: OAI/MeasureTheory/FalconerCompletion/Measures/StartingPairCompletion.lean:114 (different declaration text). Qualify references as OAI.Falconer.distanceSet@path.
```
def distanceSet {X : Type*} [PseudoMetricSpace X] (E : Set X) : Set ℝ :=
…
```
def OAI.Falconer.MainTarget line 33
Source documentation
The Falconer distance conjecture in every ambient dimension at least two.
```
def MainTarget : Prop :=
…
```
theorem OAI.Falconer.distanceSet_eq_image line 40
Distinct definitions of this name: OAI/MeasureTheory/FalconerCompletion/Measures/StartingPairCompletion.lean:121 (different declaration text). Qualify references as OAI.Falconer.distanceSet_eq_image@path.
theorem OAI.Falconer.distanceSet_isCompact line 49
Distinct definitions of this name: OAI/MeasureTheory/FalconerCompletion/Measures/StartingPairCompletion.lean:130 (different declaration text). Qualify references as OAI.Falconer.distanceSet_isCompact@path.
theorem OAI.Falconer.distanceSet_mono line 54
theorem OAI.Falconer.distanceSet_image_isometry line 60
Source documentation
Isometries, unlike auxiliary orthogonal projections, preserve distances.
```
theorem distanceSet_image_isometry {f : X → Y} (hf : Isometry f) (E : Set X) :
    distanceSet (f '' E) = distanceSet E := by
…
```

theorem OAI.Falconer.positive_distance_of_isometric_model line 71

Source documentation

Transport a distance theorem through an isometric coordinate chart.

theorem positive_distance_of_isometric_model {E : Set X} {F : Set Y}
    {f : Y → X} (hf : Isometry f) (hFE : f '' F ⊆ E)
    (hF : 0 < volume (distanceSet F)) : 0 < volume (distanceSet E) := by
…

theorem OAI.Falconer.positive_volume_of_carried_measure line 85

Source documentation

A nonzero absolutely continuous measure carried by a set forces positive Lebesgue measure.

theorem positive_volume_of_carried_measure (D : Set ℝ) (τ : Measure ℝ)
    (hmass : 0 < τ univ) (hcarried : τ Dᶜ = 0) (hac : τ ≪ volume) :
    0 < volume D := by
…

def OAI.Falconer.distanceWeight line 97
Source documentation
The weight in the classical threshold argument, and in the spherical stationary-phase normalization, is dist ^ (-(d-1)/2).
```
noncomputable def distanceWeight (a : ℝ) (z : X × X) : ℝ≥0∞ :=
…
```
def OAI.Falconer.weightedDistance line 100
theorem OAI.Falconer.weightedDistance_mass line 103
theorem OAI.Falconer.weightedDistance_mass_bounds line 109
theorem OAI.Falconer.weightedDistance_positive_finite line 134
theorem OAI.Falconer.weightedDistance_carried line 143
theorem OAI.Falconer.product_carried line 154

theorem OAI.Falconer.positive_distance_of_weighted_ac line 169

Source documentation

The dimension-independent final reduction to absolute continuity of the original weighted distance pushforward. No Fourier estimate is assumed here.

theorem positive_distance_of_weighted_ac {a : ℝ} (ha : 0 ≤ a)
    (μ ν : Measure X) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    {E : Set X} (hE : IsCompact E) (hμ : μ Eᶜ = 0) (hν : ν Eᶜ = 0)
    {dmin dmax : ℝ} (hmin : 0 < dmin) (hmax : 0 < dmax)
    (hsep : ∀ᵐ z ∂(μ.prod ν), dmin ≤ dist z.1 z.2 ∧ dist z.1 z.2 ≤ dmax)
    (hac : weightedDistance a (μ.prod ν) ≪ volume) :
    0 < volume (distanceSet E) := by
…

Mentions: OAI.Falconer.weightedDistance