Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.GoodLambdaStopping

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Step-1 stopping radii for the good-λ argument

This module packages the local energy whose exact stopping radii will feed the Vitali selection in the cube Calderón--Zygmund argument. It does not use a comparison estimate, a tail estimate, or a final good-λ inequality.

noncomputable def HCPolySupport.CubeCalderonZygmund.goodLambdaCombinedEnergy {d : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) (ε : ℝ) (x : Vec d) (r : ℝ) : ℝ

The combined normalized local L² energy used in the good-λ stopping construction. The square root is taken after adding the two squared energies; this is the form for which a stopping identity at level lambda gives the exact weighted-mass identity used in the level-set split.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.CubeCalderonZygmund.goodLambdaCombinedEnergy_nonneg {d : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) (ε : ℝ) (x : Vec d) (r : ℝ) : 0 ≤ goodLambdaCombinedEnergy f g ε x r

theorem HCPolySupport.CubeCalderonZygmund.continuousOn_goodLambdaCombinedEnergy {d : ℕ} [NeZero d] {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) (ε : ℝ) (hf : MeasureTheory.Integrable (fun (y : Vec d) => ‖f y‖ ^ 2) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (y : Vec d) => ‖g y‖ ^ 2) MeasureTheory.volume) (x : Vec d) : ContinuousOn (fun (r : ℝ) => goodLambdaCombinedEnergy f g ε x r) (Set.Ioi 0)

The combined normalized local energy is continuous on positive radii when both squared data fields are integrable.

theorem HCPolySupport.CubeCalderonZygmund.ae_tendsto_closedBallAverage_nhdsGT {d : ℕ} (h : Vec d → ℝ) (hh : MeasureTheory.Integrable h MeasureTheory.volume) : ∀ᵐ (x : Vec d), Filter.Tendsto (fun (r : ℝ) => closedBallAverage x r h) (nhdsWithin 0 (Set.Ioi 0)) (nhds (h x))

Lebesgue differentiation for the normalized sup-metric closed-ball average. This is the input that identifies the small-radius energy with its pointwise value almost everywhere.

theorem HCPolySupport.CubeCalderonZygmund.ae_tendsto_closedBallL2Energy_nhdsGT {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] (u : Vec d → F) (hu : MeasureTheory.Integrable (fun (y : Vec d) => ‖u y‖ ^ 2) MeasureTheory.volume) : ∀ᵐ (x : Vec d), Filter.Tendsto (fun (r : ℝ) => closedBallL2Energy u x r) (nhdsWithin 0 (Set.Ioi 0)) (nhds (‖u x‖ ^ 2))

Integrable square data has the expected almost-everywhere small-radius limit for the normalized local L² energy.

theorem HCPolySupport.CubeCalderonZygmund.ae_tendsto_goodLambdaCombinedEnergy_nhdsGT {d : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) (ε : ℝ) (hf : MeasureTheory.Integrable (fun (y : Vec d) => ‖f y‖ ^ 2) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (y : Vec d) => ‖g y‖ ^ 2) MeasureTheory.volume) : ∀ᵐ (x : Vec d), Filter.Tendsto (fun (r : ℝ) => goodLambdaCombinedEnergy f g ε x r) (nhdsWithin 0 (Set.Ioi 0)) (nhds √(‖f x‖ ^ 2 + ε⁻¹ ^ 2 * ‖g x‖ ^ 2))

The combined source energy converges almost everywhere at small radii to the corresponding pointwise combined energy.

theorem HCPolySupport.CubeCalderonZygmund.exists_stoppingRadius_of_tendsto_nhdsGT {E : ℝ → ℝ} {pointEnergy level R : ℝ} (hR : 0 < R) (hE : ContinuousOn E (Set.Ioi 0)) (hlimit : Filter.Tendsto E (nhdsWithin 0 (Set.Ioi 0)) (nhds pointEnergy)) (hpoint : level < pointEnergy) (hlarge : E R ≤ level) : ∃ (r : ℝ), 0 < r ∧ r ≤ R ∧ E r = level ∧ ∀ s ∈ Set.Icc r R, E s ≤ level

A positive-radius limit above the level and one large radius below it produce an exact last stopping radius. The small positive starting radius is obtained internally from the one-sided limit.

theorem HCPolySupport.CubeCalderonZygmund.exists_stoppingRadius_goodLambdaCombinedEnergy {d : ℕ} [NeZero d] {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) (ε : ℝ) (hf : MeasureTheory.Integrable (fun (y : Vec d) => ‖f y‖ ^ 2) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (y : Vec d) => ‖g y‖ ^ 2) MeasureTheory.volume) (x : Vec d) {level R : ℝ} (hR : 0 < R) (hlimit : Filter.Tendsto (fun (r : ℝ) => goodLambdaCombinedEnergy f g ε x r) (nhdsWithin 0 (Set.Ioi 0)) (nhds √(‖f x‖ ^ 2 + ε⁻¹ ^ 2 * ‖g x‖ ^ 2))) (hpoint : level < √(‖f x‖ ^ 2 + ε⁻¹ ^ 2 * ‖g x‖ ^ 2)) (hlarge : goodLambdaCombinedEnergy f g ε x R ≤ level) : ∃ (r : ℝ), 0 < r ∧ r ≤ R ∧ goodLambdaCombinedEnergy f g ε x r = level ∧ ∀ s ∈ Set.Icc r R, goodLambdaCombinedEnergy f g ε x s ≤ level

The stopping-radius certificate specialized to the combined local energy. For almost every centre, its limit hypothesis is supplied by ae_tendsto_goodLambdaCombinedEnergy_nhdsGT.