Published.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Published radial input for the planar Falconer application

The only input isolated here is the planar specialization of Orponen, On the dimension and smoothness of radial projections, Analysis & PDE 12 (2019), 1273–1294, proof of Theorem 1.13, equations (3.5)–(3.6). The parameters used by the application are s = 1 + δ / 2, t = 1 - δ / 4, and p = 1 + δ / 8. They satisfy the strict inequalities in (3.5). Orponen uses a distance weighted source measure; on disjoint compact supports that weight and its inverse are bounded, so finiteness of the moment is unchanged.

Prepared root measures follow from this radial moment estimate.

def OAI.PlanarFalconer.PublishedPlanarRadialMoment line 26
Source documentation
The precise finite-energy consequence of the published radial theorem used in the planar application. The source and pin laws may be interchanged.
```
def PublishedPlanarRadialMoment : Prop :=
…
```
theorem OAI.PlanarFalconer.compact_neighborhood_probability_for_published_radial line 36

theorem OAI.PlanarFalconer.source_uniform_radial_restrictions_of_published_radial line 58

Source documentation

Compact simultaneous restrictions turn the integrated published radial estimate into uniform control at every retained pin.

theorem source_uniform_radial_restrictions_of_published_radial
    (hOrponen : PublishedPlanarRadialMoment) (μ₀ ν₀ : ProbabilityMeasure Plane)
    (hμK : IsCompact (μ₀ : Measure Plane).support)
    (hνK : IsCompact (ν₀ : Measure Plane).support)
    (hsep : Disjoint (μ₀ : Measure Plane).support (ν₀ : Measure Plane).support)
    {δ C : ℝ} (hδ : 0 < δ) (hδ1 : δ < 1) (hC : 0 < C)
    (hμball : BallBound μ₀ (1+δ) C) (hνball : BallBound ν₀ (1+δ) C) :
    ∃ μ ν : ProbabilityMeasure Plane,
      IsCompact (μ : Measure Plane).support ∧ IsCompact (ν : Measure Plane).support ∧
      (μ : Measure Plane).support ⊆ (μ₀ : Measure Plane).support ∧
      (ν : Measure Plane).support ⊆ (ν₀ : Measure Plane).support ∧
      ∃ D : ℝ, 0 < D ∧ BallBound μ (1+δ) D ∧ BallBound ν (1+δ) D ∧
…

Mentions: OAI.PlanarFalconer.PublishedPlanarRadialMoment, OAI.PlanarFalconer.Plane, OAI.PlanarFalconer.BallBound

theorem OAI.PlanarFalconer.exists_normalized_root_setup_of_published_radial line 87