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

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

Finite-p transport under Dirichlet odd reflection

The Dirichlet odd reflection acts by coordinate signs on the gradient profile. Those signs are Euclidean isometries. Combined with the measure-preserving cell fold maps, this gives exact finite-p transport from a cube to its full reflection block.

theorem HCPolySupport.lintegral_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionVectorField_comp_norm {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) (Φ : ℝ → ENNReal) : ∫⁻ (x : Vec d) in cubeFaceReflectionBlockSet Q, Φ ‖HilbertVec.ofVec (cubeDirichletOddReflectionVectorField Q G x)‖ = 3 ^ d * ∫⁻ (y : Vec d) in openCubeSet Q, Φ ‖HilbertVec.ofVec (G y)‖

The full Dirichlet reflection block consists of exactly 3^d radial copies of the source cube. No integrability or measurability hypothesis is needed for this nonnegative integral identity.

theorem HCPolySupport.aestronglyMeasurable_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionVectorField {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (hG : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (G x)) (MeasureTheory.volume.restrict (openCubeSet Q))) : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField Q G x)) (MeasureTheory.volume.restrict (cubeFaceReflectionBlockSet Q))

Strong measurability transports from a source cube to the full Dirichlet reflection block.

theorem HCPolySupport.eLpNorm_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionVectorField {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) (p : FiniteLpExponent) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField Q G x)) p.exponent (MeasureTheory.volume.restrict (cubeFaceReflectionBlockSet Q)) = (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (G x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet Q))

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

theorem HCPolySupport.memLp_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionVectorField {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (p : FiniteLpExponent) (hG : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (G x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet Q))) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField Q G x)) p.exponent (MeasureTheory.volume.restrict (cubeFaceReflectionBlockSet Q))

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

theorem HCPolySupport.eLpNorm_openCubeSet_succ_originCube_cubeDirichletOddReflectionVectorField {d : ℕ} {m : ℤ} (G : Vec d → Vec d) (p : FiniteLpExponent) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField (originCube d m) G x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1)))) = (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (G x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))

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

theorem HCPolySupport.memLp_openCubeSet_succ_originCube_cubeDirichletOddReflectionVectorField {d : ℕ} {m : ℤ} {G : Vec d → Vec d} (p : FiniteLpExponent) (hG : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (G x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField (originCube d m) G x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1))))

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

theorem HCPolySupport.lintegral_openCubeSet_succ_originCube_cubeDirichletOddReflectionVectorField_comp_norm {d : ℕ} {m : ℤ} (G : Vec d → Vec d) (Φ : ℝ → ENNReal) : ∫⁻ (x : Vec d) in openCubeSet (originCube d (m + 1)), Φ ‖HilbertVec.ofVec (cubeDirichletOddReflectionVectorField (originCube d m) G x)‖ = 3 ^ d * ∫⁻ (y : Vec d) in openCubeSet (originCube d m), Φ ‖HilbertVec.ofVec (G y)‖

Radial nonnegative integrals on a centered parent cube are exactly 3^d times the corresponding source-cube integrals under Dirichlet odd reflection.

theorem HCPolySupport.aestronglyMeasurable_openCubeSet_succ_originCube_cubeDirichletOddReflectionVectorField {d : ℕ} {m : ℤ} {G : Vec d → Vec d} (hG : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (G x)) (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))) : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField (originCube d m) G x)) (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1))))

Strong measurability transports from a centered source cube to its parent under Dirichlet odd reflection.

theorem HCPolySupport.eLpNorm_normalizedCubeMeasure_succ_originCube_cubeDirichletOddReflectionVectorField {d : ℕ} {m : ℤ} (G : Vec d → Vec d) (p : FiniteLpExponent) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField (originCube d m) G x)) p.exponent (normalizedCubeMeasure (originCube d (m + 1))) = MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (G x)) p.exponent (normalizedCubeMeasure (originCube d m))

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

theorem HCPolySupport.memLp_normalizedCubeMeasure_succ_originCube_cubeDirichletOddReflectionVectorField {d : ℕ} {m : ℤ} {G : Vec d → Vec d} (p : FiniteLpExponent) (hG : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (G x)) p.exponent (normalizedCubeMeasure (originCube d m))) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField (originCube d m) G x)) p.exponent (normalizedCubeMeasure (originCube d (m + 1)))

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

theorem HCPolySupport.eLpNorm_cubeFaceReflectionCellCube_cubeDirichletOddReflectionVectorField {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (choice : Fin d → Fin 3) (p : FiniteLpExponent) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField Q G x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (cubeFaceReflectionCellCube Q choice))) = MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (G x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet Q))

On one reflection cell, the odd-reflected Euclidean vector field has the same finite-p norm as the original field on the source cube.