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

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

Geometric and measure-local preparation for the one-stopping-ball tail

The final tail comparison is made on the open depth descendant. These lemmas keep the two nontrivial localisation facts explicit: that descendant is inside the PDE comparison parent, and its boundary can be changed to the closed stopping ball for any square-weighted measure based on volume.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparison_descendant_subset_parent {d : ℕ} (x : Vec d) {r : ℝ} (hr : 0 < r) (depth : ℕ) : axisCube (axisCubeConcentricDepthCorner (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) depth) (axisCubeConcentricDepthSide (stoppingComparisonParentSide r depth) depth) ⊆ axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth)

The open depth descendant lies in its comparison parent.

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_tail_descendant_eq_closedBall {d : ℕ} [NeZero d] {E : Type u_1} [NormedAddCommGroup E] (f : Vec d → E) (x : Vec d) {r : ℝ} (hr : 0 < r) (depth : ℕ) (T : Set (Vec d)) : (sqWeightedMeasure f MeasureTheory.volume) (T ∩ axisCube (axisCubeConcentricDepthCorner (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) depth) (axisCubeConcentricDepthSide (stoppingComparisonParentSide r depth) depth)) = (sqWeightedMeasure f MeasureTheory.volume) (T ∩ Metric.closedBall x (5 * r))

The final square-weighted tail may cross from the open harmonic-gain descendant to the closed stopping ball without a comparison loss.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparison_descendant_side_eq {r : ℝ} (depth : ℕ) : axisCubeConcentricDepthSide (stoppingComparisonParentSide r depth) depth = 10 * r

The depth descendant used by the harmonic gain has side 10 r.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparison_parent_side_eq {r : ℝ} (depth : ℕ) : stoppingComparisonParentSide r depth = 10 * 3 ^ depth * r

The parent side is 10 * 3^n * r, the raw volume factor used for the correction-energy contribution.

theorem HCPolySupport.CubeCalderonZygmund.local_lintegral_error_eq_harmonicCorrection {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {B : Set (Vec d)} {f v w : Vec d → E} (hfu : f =ᵐ[MeasureTheory.volume.restrict B] v + w) : ∫⁻ (y : Vec d) in B, ENNReal.ofReal (‖f y - v y‖ ^ 2) = ∫⁻ (y : Vec d) in B, ENNReal.ofReal (‖w y‖ ^ 2)

On the comparison descendant, replacing the global field by the weak solution gradient turns the comparison error into the zero-trace correction. This is the restricted-a.e. transport used in the correction tail.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparison_correction_descendant_le_parent {d : ℕ} (x : Vec d) {r : ℝ} (hr : 0 < r) (depth : ℕ) (w : H10Function (axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth))) {B : ENNReal} (hB : MeasureTheory.eLpNorm (hilbertifyVecField w.grad) 2 (axisCubeNormalizedMeasure (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth)) ≤ B) : ∫⁻ (y : Vec d) in axisCube (axisCubeConcentricDepthCorner (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) depth) (axisCubeConcentricDepthSide (stoppingComparisonParentSide r depth) depth), ENNReal.ofReal (‖hilbertifyVecField w.grad y‖ ^ 2) ≤ ENNReal.ofReal (stoppingComparisonParentSide r depth ^ d) * B ^ 2

The correction integral on the descendant is bounded by its exact raw parent-cube energy.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparison_harmonic_raw_bound {d : ℕ} {q : FiniteLpExponent} (x : Vec d) {r : ℝ} (hr : 0 < r) (depth : ℕ) (v : Vec d → HilbertVec d) {B : ENNReal} (hB : MeasureTheory.eLpNorm v q.exponent (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) depth) (axisCubeConcentricDepthSide (stoppingComparisonParentSide r depth) depth)) ≤ B) : ∫⁻ (y : Vec d) in axisCube (axisCubeConcentricDepthCorner (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) depth) (axisCubeConcentricDepthSide (stoppingComparisonParentSide r depth) depth), ENNReal.ofReal (‖v y‖ ^ q.exponent.toReal) ≤ ENNReal.ofReal ((10 * r) ^ d) * B ^ q.exponent.toReal

The harmonic gain gives its raw descendant L^q integral with precisely the side-10r volume factor.

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_oneStoppingBall_le {d : ℕ} [NeZero d] {q : FiniteLpExponent} {depth : ℕ} (G : INTERNAL.HarmonicEuclideanGradientGain d q depth) (hq : 2 < q.exponent.toReal) (x : Vec d) {r R sigma0 eps M level : ℝ} (hr : 0 < r) (hsigma0 : 0 < sigma0) (heps : 0 < eps) (heps_one : eps ≤ 1) (hM : 0 < M) (hlevel : 0 < level) (hcutoff : r ≤ R / (10 * 3 ^ depth)) (f : Vec d → HilbertVec d) (H : Vec d → Vec d) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hH : MeasureTheory.MemLp (hilbertifyVecField H) 2 MeasureTheory.volume) (u : H1Function (axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth))) (hfu : f =ᵐ[MeasureTheory.volume.restrict (axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth))] hilbertifyVecField u.grad) (hweak : ∀ (phi : Vec d → ℝ), ContDiff ℝ (↑⊤) phi → HasCompactSupport phi → tsupport phi ⊆ axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) → sigma0 * ∫ (y : Vec d) in axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth), vecDot (u.grad y) (euclideanGradient phi y) = -∫ (y : Vec d) in axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth), vecDot (H y) (euclideanGradient phi y)) (hstop : goodLambdaCombinedEnergy f (sigma0⁻¹ • hilbertifyVecField H) eps x r = level) (hlast : ∀ s ∈ Set.Icc r R, goodLambdaCombinedEnergy f (sigma0⁻¹ • hilbertifyVecField H) eps x s ≤ level) : (sqWeightedMeasure f MeasureTheory.volume) ({y : Vec d | M * level < ‖f y‖} ∩ Metric.closedBall x (5 * r)) ≤ oneStoppingBallCoefficient depth G * (ENNReal.ofReal ((M / 2) ^ (2 - q.exponent.toReal)) + ENNReal.ofReal (eps ^ 2)) * ((sqWeightedMeasure f MeasureTheory.volume) ({y : Vec d | level / 2 < ‖f y‖} ∩ Metric.closedBall x r) + ENNReal.ofReal (eps⁻¹ ^ 2) * (sqWeightedMeasure (sigma0⁻¹ • hilbertifyVecField H) MeasureTheory.volume) ({y : Vec d | eps * level / 2 < ‖(sigma0⁻¹ • hilbertifyVecField H) y‖} ∩ Metric.closedBall x r))

The complete one-stopping-ball weighted comparison estimate. The harmonic comparison is constructed from the weak equation, rather than supplied as a hypothesis.