Coarse-graining support: Support.Sobolev.Foundations.CubeDirichletH2.ReflectionScalarFiniteP

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Finite-p scalar transport under Dirichlet odd reflection

The scalar Dirichlet odd reflection differs from pullback by the affine cell fold only by a sign of norm one. Combined with the measure-preserving cell fold maps, this gives exact finite-p transport from a cube to its full reflection block and exact preservation of normalized finite-p norms between centered origin cubes.

theorem HCPolySupport.eLpNorm_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionScalar {d : ℕ} (Q : TriadicCube d) (F : Vec d → ℝ) (p : FiniteLpExponent) : MeasureTheory.eLpNorm (cubeDirichletOddReflectionScalar Q F) p.exponent (MeasureTheory.volume.restrict (cubeFaceReflectionBlockSet Q)) = (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm F p.exponent (MeasureTheory.volume.restrict (openCubeSet Q))

The finite-p norm of the odd-reflected scalar on the full reflection block is exactly the 3^d measure-scaling factor times the source norm.

theorem HCPolySupport.memLp_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionScalar {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (p : FiniteLpExponent) (hF : MeasureTheory.MemLp F p.exponent (MeasureTheory.volume.restrict (openCubeSet Q))) : MeasureTheory.MemLp (cubeDirichletOddReflectionScalar Q F) p.exponent (MeasureTheory.volume.restrict (cubeFaceReflectionBlockSet Q))

Finite-p scalar integrability transports from a cube to the complete Dirichlet odd-reflection block.

theorem HCPolySupport.eLpNorm_openCubeSet_succ_originCube_cubeDirichletOddReflectionScalar {d : ℕ} {m : ℤ} (F : Vec d → ℝ) (p : FiniteLpExponent) : MeasureTheory.eLpNorm (cubeDirichletOddReflectionScalar (originCube d m) F) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1)))) = (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm F p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))

On a centered origin cube, the odd-reflected scalar has the same exact unnormalized finite-p scaling on the parent cube.

theorem HCPolySupport.memLp_openCubeSet_succ_originCube_cubeDirichletOddReflectionScalar {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (p : FiniteLpExponent) (hF : MeasureTheory.MemLp F p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))) : MeasureTheory.MemLp (cubeDirichletOddReflectionScalar (originCube d m) F) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1))))

Finite-p scalar integrability transports from an origin cube to its centered parent under Dirichlet odd reflection.

theorem HCPolySupport.eLpNorm_normalizedCubeMeasure_succ_originCube_cubeDirichletOddReflectionScalar {d : ℕ} {m : ℤ} (F : Vec d → ℝ) (p : FiniteLpExponent) : MeasureTheory.eLpNorm (cubeDirichletOddReflectionScalar (originCube d m) F) p.exponent (normalizedCubeMeasure (originCube d (m + 1))) = MeasureTheory.eLpNorm F p.exponent (normalizedCubeMeasure (originCube d m))

Normalized origin-cube finite-p scalar norms are exactly preserved by Dirichlet odd reflection from a cube to its centered parent.

theorem HCPolySupport.memLp_normalizedCubeMeasure_succ_originCube_cubeDirichletOddReflectionScalar {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (p : FiniteLpExponent) (hF : MeasureTheory.MemLp F p.exponent (normalizedCubeMeasure (originCube d m))) : MeasureTheory.MemLp (cubeDirichletOddReflectionScalar (originCube d m) F) p.exponent (normalizedCubeMeasure (originCube d (m + 1)))

Finite-p scalar integrability is preserved by normalized origin-cube odd-reflection transport.