Coarse-graining support: #
Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectionHessianRowWeightedTail
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Square-weighted tails of reflected Hessian rows #
The mixed-parity reflection of a Hessian row has the same pointwise Euclidean norm as the ordinary odd reflection of the source row. Consequently its square-weighted level tail on an origin-cube parent is exactly the existing odd-vector tail, with no new measure decomposition.
theorem
HCPolySupport.CubeCalderonZygmund.reflectedHessianRow_sqWeightedMeasure_parent_tail
{d : ℕ}
{m : ℤ}
(i : Fin d)
(R : Vec d → Vec d)
{a : ℝ}
(hR :
MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (R x))
(MeasureTheory.volume.restrict (openCubeSet (originCube d m))))
:
(sqWeightedMeasure
(fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i R x))
MeasureTheory.volume)
({x : Vec d | a < ‖HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i R x)‖} ∩ openCubeSet (originCube d (m + 1))) = 3 ^ d * (sqWeightedMeasure (fun (x : Vec d) => HilbertVec.ofVec (R x)) MeasureTheory.volume)
({x : Vec d | a < ‖HilbertVec.ofVec (R x)‖} ∩ openCubeSet (originCube d m))
The square-weighted Hessian-row tail on a centered parent is exactly
3^d copies of its source-row tail.
theorem
HCPolySupport.CubeCalderonZygmund.reflectedHessianRow_sqWeightedMeasure_innerHalf_tail_le
{d : ℕ}
{m : ℤ}
(i : Fin d)
(R : Vec d → Vec d)
{a : ℝ}
(hR :
MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (R x))
(MeasureTheory.volume.restrict (openCubeSet (originCube d m))))
:
(sqWeightedMeasure
(fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i R x))
MeasureTheory.volume)
({x : Vec d | a < ‖HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i R x)‖} ∩ scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) ≤ 3 ^ d * (sqWeightedMeasure (fun (x : Vec d) => HilbertVec.ofVec (R x)) MeasureTheory.volume)
({x : Vec d | a < ‖HilbertVec.ofVec (R x)‖} ∩ openCubeSet (originCube d m))
The Hessian-row tail on the half-scaled parent is bounded by the same
3^d source-row tail as the full reflected parent.