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

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

The one-stopping-ball comparison estimate

This is the local, genuinely PDE-derived step in the cube good-lambda argument. At an exact stopping radius it constructs the zero-trace harmonic replacement on the comparison parent, applies the finite-exponent harmonic gain on its triadic descendant, and then applies the weighted comparison-tail inequality. No harmonic comparison or tail estimate is an input hypothesis.

The datum in the stopping energy is sigma0⁻¹ • hilbertifyVecField H. This normalization is essential: it makes every constant below independent of the ellipticity scale, while the final source norm has exactly the expected sigma0⁻¹ factor.

noncomputable def HCPolySupport.CubeCalderonZygmund.oneStoppingBallCoefficient {d : ℕ} {q : FiniteLpExponent} (depth : ℕ) (G : INTERNAL.HarmonicEuclideanGradientGain d q depth) : ENNReal

The coefficient produced by the one-ball comparison. The first summand comes from the harmonic L^q gain on B_(5r), the second from the zero-trace correction energy on its comparison parent. In the final tail bound it multiplies the factored quantity (M / 2)^(2-q) + eps^2; keeping this source-facing factor separate is what allows the later good-lambda parameter choice.

Equations

• HCPolySupport.CubeCalderonZygmund.oneStoppingBallCoefficient depth G = 4 * 5 ^ d * (2 * (G.constantValue * ↑d)) ^ q.exponent.toReal + 12 * ENNReal.ofReal ((5 * 3 ^ depth) ^ d)

theorem HCPolySupport.CubeCalderonZygmund.oneStoppingBallCoefficient_ne_top {d : ℕ} {q : FiniteLpExponent} {depth : ℕ} (G : INTERNAL.HarmonicEuclideanGradientGain d q depth) : oneStoppingBallCoefficient depth G ≠ ⊤

The coefficient is finite; hence it may safely be used in the later weighted layer-cake integration without an implicit extended-real exception.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParent_eLpNorm_two_bounds_of_stop_lastExit {d : ℕ} [NeZero d] {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) {eps level r R : ℝ} (heps : 0 < eps) (hr : 0 < r) (depth : ℕ) (hcutoff : r ≤ R / (10 * 3 ^ depth)) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (x : Vec d) (hlast : ∀ s ∈ Set.Icc r R, goodLambdaCombinedEnergy f g eps x s ≤ level) : MeasureTheory.eLpNorm f 2 (axisCubeNormalizedMeasure (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth)) ≤ ENNReal.ofReal level ∧ MeasureTheory.eLpNorm g 2 (axisCubeNormalizedMeasure (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth)) ≤ ENNReal.ofReal (eps * level)

The exact stopping identity and the last-exit bound control both fields on the actual harmonic-comparison parent. This is deliberately stated before the PDE comparison: it is the point at which the conservative radius cutoff is converted into the sharp parent-radius input required by the local replacement.

theorem HCPolySupport.CubeCalderonZygmund.exists_stoppingComparison_harmonic_remainder {d : ℕ} [NeZero d] {q : FiniteLpExponent} {depth : ℕ} (G : INTERNAL.HarmonicEuclideanGradientGain d q depth) (x : Vec d) {r R sigma0 eps level : ℝ} (hr : 0 < r) (hsigma0 : 0 < sigma0) (heps : 0 < eps) (heps_one : eps ≤ 1) (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)) (hlast : ∀ s ∈ Set.Icc r R, goodLambdaCombinedEnergy f (sigma0⁻¹ • hilbertifyVecField H) eps x s ≤ level) : ∃ (w : H10Function (axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth))), WeakPoissonEquationOn (axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth)) (u - w.toH1Function) 0 ∧ MeasureTheory.eLpNorm (hilbertifyVecField w.grad) 2 (axisCubeNormalizedMeasure (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth)) ≤ ENNReal.ofReal (eps * level) ∧ MeasureTheory.MemLp (hilbertifyVecField (u - w.toH1Function).grad) q.exponent (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) depth) (axisCubeConcentricDepthSide (stoppingComparisonParentSide r depth) depth)) ∧ MeasureTheory.eLpNorm (hilbertifyVecField (u - w.toH1Function).grad) q.exponent (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) depth) (axisCubeConcentricDepthSide (stoppingComparisonParentSide r depth) depth)) ≤ 2 * (G.constantValue * ↑d) * ENNReal.ofReal level

The PDE part of the one-ball argument. The zero-trace correction and its harmonic remainder are constructed internally; the returned bounds are the two inputs needed by the weighted-tail step.