Coarse-graining support: #
Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectionScalarWeightedTail
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Square-weighted tails of reflected scalars #
Scalar odd reflection preserves square-weighted level tails up to the exact
3^d parent-volume factor. The proof embeds the scalar into one coordinate
of the existing reflected-vector API; the zero-dimensional case is direct.
theorem
HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_openCubeSet_succ_originCube_cubeDirichletOddReflectionScalar_tail
{d : ℕ}
{m : ℤ}
(F : Vec d → ℝ)
{a : ℝ}
(hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (openCubeSet (originCube d m))))
:
(sqWeightedMeasure (cubeDirichletOddReflectionScalar (originCube d m) F) MeasureTheory.volume)
({x : Vec d | a < ‖cubeDirichletOddReflectionScalar (originCube d m) F x‖} ∩ openCubeSet (originCube d (m + 1))) = 3 ^ d * (sqWeightedMeasure F MeasureTheory.volume) ({x : Vec d | a < ‖F x‖} ∩ openCubeSet (originCube d m))
A square-weighted norm tail of the scalar Dirichlet odd reflection on a
centered parent cube is exactly 3^d copies of its source-cube tail.
theorem
HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_innerHalf_succ_originCube_cubeDirichletOddReflectionScalar_tail_le
{d : ℕ}
{m : ℤ}
(F : Vec d → ℝ)
{a : ℝ}
(hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (openCubeSet (originCube d m))))
:
(sqWeightedMeasure (cubeDirichletOddReflectionScalar (originCube d m) F) MeasureTheory.volume)
({x : Vec d | a < ‖cubeDirichletOddReflectionScalar (originCube d m) F x‖} ∩ scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) ≤ 3 ^ d * (sqWeightedMeasure F MeasureTheory.volume) ({x : Vec d | a < ‖F x‖} ∩ openCubeSet (originCube d m))
The square-weighted scalar-reflection tail on the half-scaled parent is
bounded by the exact 3^d source-cube tail.