ReflectedOneLevelTail #
Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.
The centered-Neumann reflected one-level good-lambda inequality #
Even reflection, extension by zero, global stopping, local harmonic comparison,
and Vitali selection are all constructed internally from the source Neumann
weak solution and its L² datum.
theorem
HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_neumannReflected_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 : H1MeanZeroFunction (openCubeSet (originCube d m)))
(H : Vec d → Vec d)
(hH : MemVectorL2 (openCubeSet (originCube d m)) H)
(hweak :
IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) u
fun (x : Vec d) => -H x)
(hlevel : neumannReflectedGoodLambdaCutoff m depth eps sigma0 u H < level)
:
(sqWeightedMeasure (hilbertifyVecField u.toH1Function.grad) MeasureTheory.volume)
({x : Vec d | M * level < ‖hilbertifyVecField u.toH1Function.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.toH1Function.grad) MeasureTheory.volume)
({x : Vec d | level / 2 < ‖hilbertifyVecField u.toH1Function.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-Neumann one-level good-lambda bound obtained from the
even-reflected parent problem.