RadialMoments.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

From radial projection moments to integer cap availability

The radial pushforwards form a Markov kernel. Mathlib's kernel Radon--Nikodym derivative supplies a jointly measurable version of all their angular densities, so separate choices of densities are unnecessary. This connects the published radial-moment input to the truncation step.

def OAI.Falconer.radialKernel line 22
Source documentation
The radial projection law, with the pin as its kernel parameter.
```
noncomputable def radialKernel {d : ℕ} (ν : ProbabilityMeasure (Space d)) :
    Kernel (Space d) (Space d) :=
…
```
Mentions: OAI.Falconer.Space
instance OAI.Falconer.(instance at line 28) line 28
theorem OAI.Falconer.radialKernel_apply line 32
def OAI.Falconer.radialKernelDensity line 44
Source documentation
A single jointly measurable choice of the radial angular densities.
```
noncomputable def radialKernelDensity {d : ℕ} (ν : ProbabilityMeasure (Space d))
    (σ : Measure (Space d)) : Space d × Space d → ℝ≥0∞ :=
…
```
Mentions: OAI.Falconer.Space
theorem OAI.Falconer.measurable_radialKernelDensity line 48
theorem OAI.Falconer.radialKernelDensity_withDensity line 53
theorem OAI.Falconer.radialKernelDensity_moment line 65

theorem OAI.Falconer.radial_rnDeriv_moment_eq_norm line 78

Source documentation

The moment written as an integral of the density agrees with the published convention of taking the pth power of its Lᵖ norm.

theorem radial_rnDeriv_moment_eq_norm {d : ℕ} (ν : ProbabilityMeasure (Space d))
    (σ : Measure (Space d)) [IsFiniteMeasure σ] (x : Space d)
    {p : ℝ} (hp : 0 < p) :
    (∫⁻ a, ((ν : Measure (Space d)).map (radialDirection x)).rnDeriv σ a ^ p ∂σ) =
      (eLpNorm (fun a => (((ν : Measure (Space d)).map
        (radialDirection x)).rnDeriv σ a).toReal) (ENNReal.ofReal p) σ) ^ p := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.radialDirection

theorem OAI.Falconer.capAvailable_of_radial_moments line 100

Source documentation

A.e. absolute continuity and integrated radial pth moments imply the integer cap conclusion. These are precisely the density data used from the radial projection input; the geometric cap bound on σ is explicit.

theorem capAvailable_of_radial_moments {d : ℕ}
    (μ ν : ProbabilityMeasure (Space d)) (σ : Measure (Space d)) [IsFiniteMeasure σ]
    (hν : ∀ᵐ x ∂(μ : Measure (Space d)),
      (ν : Measure (Space d)).map (radialDirection x) ≪ σ)
    (hμ : ∀ᵐ y ∂(ν : Measure (Space d)),
      (μ : Measure (Space d)).map (radialDirection y) ≪ σ)
    {p q A : ℝ} (hp : 1 < p) (hA : 0 < A)
    (hσ : ∀ w : Space d, ‖w‖ = 1 → ∀ u : ℝ, 0 < u → u ≤ 1 →
      σ (Metric.ball w u) ≤ ENNReal.ofReal (A * u ^ q))
    (hmoment : ((∫⁻ x, ∫⁻ a,
      ((ν : Measure (Space d)).map (radialDirection x)).rnDeriv σ a ^ p ∂σ
        ∂(μ : Measure (Space d))) +
…

Mentions: OAI.Falconer.Space, OAI.Falconer.radialDirection

theorem OAI.Falconer.capAvailable_of_radial_Lp_moments line 129

Source documentation

The same consequence in the integrated Lᵖ norm notation of the published radial projection estimate.

theorem capAvailable_of_radial_Lp_moments {d : ℕ}
    (μ ν : ProbabilityMeasure (Space d)) (σ : Measure (Space d)) [IsFiniteMeasure σ]
    (hν : ∀ᵐ x ∂(μ : Measure (Space d)),
      (ν : Measure (Space d)).map (radialDirection x) ≪ σ)
    (hμ : ∀ᵐ y ∂(ν : Measure (Space d)),
      (μ : Measure (Space d)).map (radialDirection y) ≪ σ)
    {p q A : ℝ} (hp : 1 < p) (hA : 0 < A)
    (hσ : ∀ w : Space d, ‖w‖ = 1 → ∀ u : ℝ, 0 < u → u ≤ 1 →
      σ (Metric.ball w u) ≤ ENNReal.ofReal (A * u ^ q))
    (hmoment : ((∫⁻ x,
      (eLpNorm (fun a => (((ν : Measure (Space d)).map
        (radialDirection x)).rnDeriv σ a).toReal) (ENNReal.ofReal p) σ) ^ p
…

Mentions: OAI.Falconer.Space, OAI.Falconer.radialDirection