IntegerCaps.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Integer cap availability from radial densities

This is the measure-theoretic truncation step of prep:integer-caps. An angular reference measure with cap exponent q and integrable radial pth density moments give availability of q for the original pair law. The radial density hypothesis is the input supplied by the radial projection theorem.

theorem OAI.Falconer.density_threshold_cap_scalar line 19
theorem OAI.Falconer.truncated_radial_cap_of_density line 31

theorem OAI.Falconer.capAvailable_of_bilateral_radial_densities line 67

Source documentation

Bilateral radial densities with finite integrated pth moments make the reference cap exponent available in the original product measure. The deleted mass has a positive power saving for every requested loss. Null strips of exceptional pins make the resulting bounds valid at every support pin, although the radial density identities hold only almost everywhere.

theorem capAvailable_of_bilateral_radial_densities {d : ℕ}
    (μ ν : ProbabilityMeasure (Space d)) (σ : Measure (Space d))
    (f g : Space d × Space d → ℝ≥0∞) (hf : Measurable f) (hg : Measurable g)
    (hfdensity : ∀ᵐ x ∂(μ : Measure (Space d)),
      (ν : Measure (Space d)).map (radialDirection x) =
        σ.withDensity (fun a => f (x, a)))
    (hgdensity : ∀ᵐ y ∂(ν : Measure (Space d)),
      (μ : Measure (Space d)).map (radialDirection y) =
        σ.withDensity (fun a => g (y, a)))
    {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))
…

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

theorem OAI.Falconer.capAvailable_of_bilateral_radial_densities_restrict line 173

Source documentation

The same density truncation works inside every measurable coarse pair filter; its fibers continue to use the original source marginals.

theorem capAvailable_of_bilateral_radial_densities_restrict {d : ℕ}
    (μ ν : ProbabilityMeasure (Space d)) (σ : Measure (Space d))
    (f g : Space d × Space d → ℝ≥0∞) (hf : Measurable f) (hg : Measurable g)
    (hfdensity : ∀ᵐ x ∂(μ : Measure (Space d)),
      (ν : Measure (Space d)).map (radialDirection x) =
        σ.withDensity (fun a => f (x, a)))
    (hgdensity : ∀ᵐ y ∂(ν : Measure (Space d)),
      (μ : Measure (Space d)).map (radialDirection y) =
        σ.withDensity (fun a => g (y, a)))
    {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))
…

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