Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.InteriorOneLevelTail #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
An interior one-level cube good-lambda inequality #
This file assembles the global stopping family, the local one-ball comparison, and the Vitali cover for a solution on an arbitrary open parent set. The comparison-parent containment and the global energy cutoff remain explicit internal hypotheses. Consequently, the result is an internal conditional assembly theorem, not a source-facing Calderon--Zygmund estimate.
theorem
HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_openParent_oneLevel_tail_originCube
{d : ℕ}
[NeZero d]
{q : FiniteLpExponent}
{depth : ℕ}
(G : INTERNAL.HarmonicEuclideanGradientGain d q depth)
(hq : 2 < q.exponent.toReal)
{U : Set (Vec d)}
(hU : IsOpen U)
{m : ℤ}
{sigma0 eps M level : ℝ}
(hsigma0 : 0 < sigma0)
(heps : 0 < eps)
(heps_one : eps ≤ 1)
(hM : 1 ≤ M)
(uU : H1Function U)
(H : Vec d → Vec d)
(hH : MemVectorL2 U H)
(hweak :
∀ (phi : Vec d → ℝ),
ContDiff ℝ (↑⊤) phi →
HasCompactSupport phi →
tsupport phi ⊆ U →
sigma0 * ∫ (y : Vec d) in U, vecDot (uU.grad y) (euclideanGradient phi y) = -∫ (y : Vec d) in U, vecDot (H y) (euclideanGradient phi y))
(hparent :
∀ x ∈ openCubeSet (originCube d m),
∀ {r : ℝ},
0 < r →
r ≤ cubeRadius (originCube d m) / (10 * 3 ^ depth) →
axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) ⊆ U)
(hcutoff :
√(((2 * (cubeRadius (originCube d m) / (10 * 3 ^ depth))) ^ d)⁻¹ * ((∫ (y : Vec d), ‖openParentGradientExtension U uU y‖ ^ 2) + eps⁻¹ ^ 2 * ∫ (y : Vec d), ‖(sigma0⁻¹ • hilbertifyVecField (openParentDatumExtension U H)) y‖ ^ 2)) < level)
:
(sqWeightedMeasure (openParentGradientExtension U uU) MeasureTheory.volume)
({x : Vec d | M * level < ‖openParentGradientExtension U uU x‖} ∩ openCubeSet (originCube d m)) ≤ oneStoppingBallCoefficient depth G * (ENNReal.ofReal ((M / 2) ^ (2 - q.exponent.toReal)) + ENNReal.ofReal (eps ^ 2)) * ((sqWeightedMeasure (openParentGradientExtension U uU) MeasureTheory.volume)
({x : Vec d | level / 2 < ‖openParentGradientExtension U uU x‖} ∩ U) + ENNReal.ofReal (eps⁻¹ ^ 2) * (sqWeightedMeasure (sigma0⁻¹ • hilbertifyVecField (openParentDatumExtension U H)) MeasureTheory.volume)
({x : Vec d | eps * level / 2 < ‖(sigma0⁻¹ • hilbertifyVecField (openParentDatumExtension U H)) x‖} ∩ U))
The one-level good-lambda tail bound for a solution on an open parent.
Stopping radii and the Vitali subfamily are constructed internally. Every local PDE input is obtained by restricting the parent weak equation.