Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectionWeightedTail #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Square-weighted tails under Dirichlet odd reflection #
The global good-λ argument works with the squared-density measure
‖f‖² dx. This file records that level tails of an odd-reflected
field on a centered parent cube are exactly 3^d copies of the corresponding
tail on the source cube.
theorem
HCPolySupport.CubeCalderonZygmund.oddReflectionVector_tail_sqWeightedMeasure_scale
{d : ℕ}
{m : ℤ}
(G : Vec d → Vec d)
{a : ℝ}
(hG :
MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (G x))
(MeasureTheory.volume.restrict (openCubeSet (originCube d m))))
:
(sqWeightedMeasure (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField (originCube d m) G x))
MeasureTheory.volume)
({x : Vec d | a < ‖HilbertVec.ofVec (cubeDirichletOddReflectionVectorField (originCube d m) G x)‖} ∩ openCubeSet (originCube d (m + 1))) = 3 ^ d * (sqWeightedMeasure (fun (x : Vec d) => HilbertVec.ofVec (G x)) MeasureTheory.volume)
({x : Vec d | a < ‖HilbertVec.ofVec (G x)‖} ∩ openCubeSet (originCube d m))
A square-weighted norm tail of the Dirichlet odd reflection on a centered
parent cube is exactly 3^d copies of the source-cube tail.