Ball integral absolute continuity

This module contains thin-shell estimates and the resulting absolute continuity of scalar ball-integral radius functions.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.dist_ballIntegral_le_radialOpenShell_integral_norm {n : ℕ} [NeZero n] {f : Domain n → ℝ} {r s R0 : ℝ} (hrR0 : r ≤ R0) (hsR0 : s ≤ R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) : dist (∫ (x : Domain n) in Metric.ball 0 r, f x) (∫ (x : Domain n) in Metric.ball 0 s, f x) ≤ ∫ (x : Domain n) in Metric.ball 0 R0, (Set.Ioo (min r s) (max r s)).indicator (fun (x : ℝ) => 1) ‖x‖ * |f x|

The difference of two ball integrals is controlled by the L¹ mass of f on the radial shell between the two radii.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.dist_ballIntegral_le_radialOpenShell_setIntegral_norm {n : ℕ} [NeZero n] {f : Domain n → ℝ} {r s R0 : ℝ} (hrR0 : r ≤ R0) (hsR0 : s ≤ R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) : dist (∫ (x : Domain n) in Metric.ball 0 r, f x) (∫ (x : Domain n) in Metric.ball 0 s, f x) ≤ ∫ (x : Domain n) in RadialOpenShell r s, |f x| ∂MeasureTheory.volume.restrict (Metric.ball 0 R0)

Set-integral form of dist_ballIntegral_le_radialOpenShell_integral_norm, with the ambient measure already restricted to the containing ball.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.sum_dist_ballIntegral_le_radialOpenShells_integral_norm {n : ℕ} [NeZero n] {f : Domain n → ℝ} {a b R0 : ℝ} {E : ℕ × (ℕ → ℝ × ℝ)} (hab : a ≤ b) (hbR0 : b ≤ R0) (hE : E ∈ AbsolutelyContinuousOnInterval.disjWithin a b) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) : ∑ i ∈ Finset.range E.1, dist (∫ (x : Domain n) in Metric.ball 0 (E.2 i).1, f x) (∫ (x : Domain n) in Metric.ball 0 (E.2 i).2, f x) ≤ ∫ (x : Domain n) in RadialOpenShells E, |f x| ∂MeasureTheory.volume.restrict (Metric.ball 0 R0)

Finite disjoint families of radius intervals give the corresponding absolute-continuity sum estimate for ball integrals.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.sum_dist_ballIntegral_le_radialOpenShells_lintegral_toReal {n : ℕ} [NeZero n] {f : Domain n → ℝ} {a b R0 : ℝ} {E : ℕ × (ℕ → ℝ × ℝ)} (hab : a ≤ b) (hbR0 : b ≤ R0) (hE : E ∈ AbsolutelyContinuousOnInterval.disjWithin a b) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) : ∑ i ∈ Finset.range E.1, dist (∫ (x : Domain n) in Metric.ball 0 (E.2 i).1, f x) (∫ (x : Domain n) in Metric.ball 0 (E.2 i).2, f x) ≤ (∫⁻ (x : Domain n) in RadialOpenShells E, ‖f x‖ₑ ∂MeasureTheory.volume.restrict (Metric.ball 0 R0)).toReal

lintegral version of the finite shell estimate, convenient for the absolute-continuity filter argument.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusAbsolutelyContinuous_of_radialOpenShellsVolumeTendstoZero {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 : ℝ} (hthin : RadialOpenShellsVolumeTendstoZero n) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) : BallIntegralRadiusAbsolutelyContinuous f R0

Thin radial-shell volume control implies absolute continuity of every L¹ ball-integral radius function.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusACOfIntegrableOnBall_of_radialOpenShellsVolumeTendstoZero {n : ℕ} (hthin : RadialOpenShellsVolumeTendstoZero n) : BallIntegralRadiusACOfIntegrableOnBall n

Packaged form: the thin radial-shell volume theorem supplies the reusable ball-integral absolute-continuity theorem.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusWeightedRepresentation_of_ac_derivativeFormula {n : ℕ} (hac_all : BallIntegralRadiusACOfIntegrableOnBall n) (hformula : BallIntegralRadiusDerivativeFormula n) : BallIntegralRadiusWeightedRepresentation n

A packaged radius-derivative formula, together with scalar radius absolute continuity, yields the unrestricted weighted radial representation by taking the representing density to be the derivative of the ball-integral radius function.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusWeightedRepresentationForWeights_of_ac_derivativeFormulaForWeights {n : ℕ} (hac_all : BallIntegralRadiusACOfIntegrableOnBall n) (hformula : BallIntegralRadiusDerivativeFormulaForWeights n) : BallIntegralRadiusWeightedRepresentationForWeights n

Restricted-weight version of ballIntegralRadiusWeightedRepresentation_of_ac_derivativeFormula.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusWeightedRepresentation_of_derivativeFormula_euclidean {n : ℕ} (hformula : BallIntegralRadiusDerivativeFormula n) : BallIntegralRadiusWeightedRepresentation n

Euclidean thin-shell absolute continuity turns an unrestricted derivative formula into the unrestricted weighted radial representation.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusWeightedRepresentationForWeights_of_derivativeFormulaForWeights_euclidean {n : ℕ} (hformula : BallIntegralRadiusDerivativeFormulaForWeights n) : BallIntegralRadiusWeightedRepresentationForWeights n

Euclidean thin-shell absolute continuity turns a restricted derivative formula into the restricted weighted radial representation.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyAbsolutelyContinuousOnRadii_of_locallyL2_radialShellsVolume {n m : ℕ} [NeZero n] {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hthin : RadialOpenShellsVolumeTendstoZero n) (hDu_meas : GradientAEStronglyMeasurableIn Du Ω) (hgrad : GradientLocallyL2In Du Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) : WeakEnergyAbsolutelyContinuousOnRadii Du R0

Local L² radius absolute continuity supplied by the thin radial-shell volume estimate.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyAbsolutelyContinuousOnRadii_of_W12LocIn_radialShellsVolume {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hthin : RadialOpenShellsVolumeTendstoZero n) (hW : W12LocIn u Du Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) : WeakEnergyAbsolutelyContinuousOnRadii Du R0

W^{1,2}_{loc} radius absolute continuity supplied by the thin radial-shell volume estimate.