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

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

Global stopping families for the cube good-λ argument

This module turns the a.e. differentiation theorem and the global L² cutoff into one radius at every relevant centre. It is deliberately independent of the PDE comparison: the returned last-exit certificates are the complete interface consumed by the later Vitali assembly.

theorem HCPolySupport.CubeCalderonZygmund.exists_globalStoppingFamily {d : ℕ} [NeZero d] {m : ℤ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (depth : ℕ) (f : Vec d → F) (g : Vec d → G) (eps M level : ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (heps : 0 < eps) (hM : 1 ≤ M) (hlevel : √(((2 * (cubeRadius (originCube d m) / (10 * 3 ^ depth))) ^ d)⁻¹ * ((∫ (y : Vec d), ‖f y‖ ^ 2) + eps⁻¹ ^ 2 * ∫ (y : Vec d), ‖g y‖ ^ 2)) < level) (target : Set (Vec d)) (htarget : ∀ x ∈ target, M * level < ‖f x‖) : ∃ (D : Set (Vec d)) (radius : Vec d → ℝ), MeasureTheory.volume Dᶜ = 0 ∧ ∀ x ∈ target ∩ D, 0 < radius x ∧ radius x ≤ cubeRadius (originCube d m) / (10 * 3 ^ depth) ∧ goodLambdaCombinedEnergy f g eps x (radius x) = level ∧ ∀ s ∈ Set.Icc (radius x) (cubeRadius (originCube d m)), goodLambdaCombinedEnergy f g eps x s ≤ level

Above the global L² cutoff, every designated high-field point has an exact stopping radius below the conservative comparison cutoff.

The differentiation set is constructed internally. The radius is a total function only to match the Vitali API; its values away from target ∩ D are irrelevant.