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

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

Large-scale inputs for continuous good-λ stopping radii

The elementary estimates here isolate the only global input in the continuous-radius stopping construction. A global squared mass bounds every normalized ball energy above a fixed positive scale; consequently the usual last-crossing construction may stop before that scale while retaining its last-exit certificate all the way to the ambient radius.

theorem HCPolySupport.CubeCalderonZygmund.closedBallL2Energy_le_globalIntegral {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] (f : Vec d → F) (hf : MeasureTheory.Integrable (fun (y : Vec d) => ‖f y‖ ^ 2) MeasureTheory.volume) (x : Vec d) {rho s : ℝ} (hrho : 0 < rho) (hrhos : rho ≤ s) : closedBallL2Energy f x s ≤ ((2 * rho) ^ d)⁻¹ * ∫ (y : Vec d), ‖f y‖ ^ 2

A global squared mass bounds every normalized closed-ball L² energy at scales at least rho.

theorem HCPolySupport.CubeCalderonZygmund.goodLambdaCombinedEnergy_le_globalIntegral {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) {rho s : ℝ} (hrho : 0 < rho) (hrhos : rho ≤ s) : goodLambdaCombinedEnergy f g ε x s ≤ √(((2 * rho) ^ d)⁻¹ * ((∫ (y : Vec d), ‖f y‖ ^ 2) + ε⁻¹ ^ 2 * ∫ (y : Vec d), ‖g y‖ ^ 2))

The good-λ combined energy is uniformly controlled at scales at least rho by the correspondingly weighted global squared mass.

theorem HCPolySupport.CubeCalderonZygmund.exists_stoppingRadius_goodLambdaCombinedEnergy_of_largeScaleBound {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 rho R : ℝ} (hrho : 0 < rho) (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)) (hrho_bound : goodLambdaCombinedEnergy f g ε x rho ≤ level) (hlarge : ∀ s ∈ Set.Icc rho R, goodLambdaCombinedEnergy f g ε x s ≤ level) : ∃ (r : ℝ), 0 < r ∧ r ≤ rho ∧ goodLambdaCombinedEnergy f g ε x r = level ∧ ∀ s ∈ Set.Icc r R, goodLambdaCombinedEnergy f g ε x s ≤ level

A local last crossing before rho remains a last exit through R when the combined energy is uniformly below the level on the large-scale interval. This is the stopping certificate used after the global-mass estimate fixes a large scale.