Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectedOneLevelTail #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
The reflected one-level cube good-λ inequality #
This is the unconditional Caffarelli--Peral one-level estimate on a centered cube. Odd reflection, extension by zero, stopping radii, local harmonic comparison, and Vitali selection are all constructed internally.
theorem
HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_reflected_oneLevel_tail_originCube
{d : ℕ}
[NeZero d]
{q : FiniteLpExponent}
{depth : ℕ}
(G : INTERNAL.HarmonicEuclideanGradientGain d q depth)
(hq : 2 < q.exponent.toReal)
{m : ℤ}
{sigma0 eps M level : ℝ}
(hsigma0 : 0 < sigma0)
(heps : 0 < eps)
(heps_one : eps ≤ 1)
(hM : 1 ≤ M)
(u : H10Function (openCubeSet (originCube d m)))
(H : Vec d → Vec d)
(hH : MemVectorL2 (openCubeSet (originCube d m)) H)
(hweak :
∀ (psi : H10Function (openCubeSet (originCube d m))),
sigma0 * ∫ (x : Vec d) in openCubeSet (originCube d m), vecDot (u.grad x) (psi.grad x) = -∫ (x : Vec d) in openCubeSet (originCube d m), vecDot (H x) (psi.grad x))
(hlevel : reflectedGoodLambdaCutoff m depth eps sigma0 u H < level)
:
(sqWeightedMeasure (hilbertifyVecField u.grad) MeasureTheory.volume)
({x : Vec d | M * level < ‖hilbertifyVecField u.grad x‖} ∩ openCubeSet (originCube d m)) ≤ 3 ^ d * oneStoppingBallCoefficient depth G * (ENNReal.ofReal ((M / 2) ^ (2 - q.exponent.toReal)) + ENNReal.ofReal (eps ^ 2)) * ((sqWeightedMeasure (hilbertifyVecField u.grad) MeasureTheory.volume)
({x : Vec d | level / 2 < ‖hilbertifyVecField u.grad x‖} ∩ openCubeSet (originCube d m)) + ENNReal.ofReal (eps⁻¹ ^ 2) * (sqWeightedMeasure (sigma0⁻¹ • hilbertifyVecField H) MeasureTheory.volume)
({x : Vec d | eps * level / 2 < ‖(sigma0⁻¹ • hilbertifyVecField H) x‖} ∩ openCubeSet (originCube d m)))
The centered-cube one-level good-λ bound obtained from the reflected
parent problem. The stopping energy is the corrected square root of the sum
of the two squared normalized energies.