ReflectionFiniteP

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Finite-p transport under Neumann even reflection

The all-face Neumann reflection acts on vector fields by the coordinate-fold linear isometries. Its Euclidean norm therefore agrees pointwise with the already-developed Dirichlet odd reflection, whose additional scalar sign has unit modulus. This file transfers the exact finite-p norm and weighted-tail identities to the even reflection used by the Neumann good-lambda argument.

theorem HCPolySupport.CubeEuclideanL2LpField.memVectorL2_openCubeSet {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (G : CubeEuclideanL2LpField Q p) : MemVectorL2 (openCubeSet Q) G.toField

The stored normalized Euclidean L² witness gives the raw vector L² datum required by the Neumann weak equation on the source open cube.

theorem HCPolySupport.norm_hilbertVec_ofVec_cubeCoordinateFoldReflectedVectorField_eq_oddReflection {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) (x : Vec d) : ‖HilbertVec.ofVec (cubeCoordinateFoldReflectedVectorField Q G x)‖ = ‖HilbertVec.ofVec (cubeDirichletOddReflectionVectorField Q G x)‖

The Neumann even reflection and Dirichlet odd reflection have the same pointwise Euclidean norm.

theorem HCPolySupport.eLpNorm_cubeCoordinateFoldReflectedVectorField_eq_oddReflection {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) (p : ENNReal) (mu : MeasureTheory.Measure (Vec d)) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeCoordinateFoldReflectedVectorField Q G x)) p mu = MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionVectorField Q G x)) p mu

Every L^p seminorm of the Neumann even reflection agrees with the corresponding Dirichlet odd-reflection seminorm.

theorem HCPolySupport.eLpNorm_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedVectorField {d : ℕ} {m : ℤ} (G : Vec d → Vec d) (p : FiniteLpExponent) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeCoordinateFoldReflectedVectorField (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)))

Exact finite-p scaling from a centered cube to its parent under Neumann even reflection.

theorem HCPolySupport.memLp_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedVectorField {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 (cubeCoordinateFoldReflectedVectorField (originCube d m) G x)) p.exponent (MeasureTheory.volume.restrict (openCubeSet (originCube d (m + 1))))

Finite-p membership transports from a centered cube to its parent under Neumann even reflection.

theorem HCPolySupport.eLpNorm_normalizedCubeMeasure_succ_originCube_cubeCoordinateFoldReflectedVectorField {d : ℕ} {m : ℤ} (G : Vec d → Vec d) (p : FiniteLpExponent) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (cubeCoordinateFoldReflectedVectorField (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 finite-p norms are exactly preserved from a centered cube to its parent under Neumann even reflection.

theorem HCPolySupport.memLp_normalizedCubeMeasure_succ_originCube_cubeCoordinateFoldReflectedVectorField {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 (cubeCoordinateFoldReflectedVectorField (originCube d m) G x)) p.exponent (normalizedCubeMeasure (originCube d (m + 1)))

Normalized finite-p membership is preserved by Neumann even reflection.

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

Radial nonnegative integrals on the reflected parent consist of exactly 3^d copies of the source-cube integral.

theorem HCPolySupport.sqWeightedMeasure_reflectedGradient_tail {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)))) : (CubeCalderonZygmund.sqWeightedMeasure (fun (x : Vec d) => HilbertVec.ofVec (cubeCoordinateFoldReflectedVectorField (originCube d m) G x)) MeasureTheory.volume) ({x : Vec d | a < ‖HilbertVec.ofVec (cubeCoordinateFoldReflectedVectorField (originCube d m) G x)‖} ∩ openCubeSet (originCube d (m + 1))) = 3 ^ d * (CubeCalderonZygmund.sqWeightedMeasure (fun (x : Vec d) => HilbertVec.ofVec (G x)) MeasureTheory.volume) ({x : Vec d | a < ‖HilbertVec.ofVec (G x)‖} ∩ openCubeSet (originCube d m))

Square-weighted level tails have the exact 3^d reflection factor under Neumann even reflection.

noncomputable def HCPolySupport.CubeEuclideanL2LpField.neumannEvenReflectionToParent {d : ℕ} {m : ℤ} {p : FiniteLpExponent} (G : CubeEuclideanL2LpField (originCube d m) p) : CubeEuclideanL2LpField (originCube d (m + 1)) p

Reflect an L² ∩ L^p datum to the centered parent cube, preserving both stored normalized memberships exactly.

Equations

• G.neumannEvenReflectionToParent = { toField := HCPolySupport.cubeCoordinateFoldReflectedVectorField (HCPolySupport.originCube d m) G.toField, euclideanMemLp := ⋯, euclideanMemL2 := ⋯ }

@[simp]

theorem HCPolySupport.CubeEuclideanL2LpField.neumannEvenReflectionToParent_toField {d : ℕ} {m : ℤ} {p : FiniteLpExponent} (G : CubeEuclideanL2LpField (originCube d m) p) : G.neumannEvenReflectionToParent.toField = cubeCoordinateFoldReflectedVectorField (originCube d m) G.toField