BoundaryOddPairing

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Folding a tested pairing across one coordinate face

Let U be invariant under the reflection in {y i = c} and let H be one of the two open halves it cuts. A flux field and a scalar source on H extend oddly across the face. Testing the extended data on U against a smooth compactly supported function is the same as testing the original data on H against the odd fold of that function. This is the pairing identity behind the reflection of a divergence-form weak solution; only measure-preservation of the reflection and the vanishing of the odd fold on the face are used.

1. The gradient leg

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.integral_vecDot_oddFaceExtendGrad_eq {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUopen : IsOpen U) {i : Fin d} {c sigma : ℝ} (hUsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection c i y ∈ U ↔ y ∈ U) {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : ∀ (j : Fin d), MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => Section4.Provider.ExcessDecay.zeroExtendGrad (Section4.Provider.ExcessDecay.faceHalf U i c sigma) F y j) 2 MeasureTheory.volume) {φ : HCPolySupport.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : ∫ (y : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (Section4.Provider.ExcessDecay.oddFaceExtendGrad c i (Section4.Provider.ExcessDecay.zeroExtendGrad (Section4.Provider.ExcessDecay.faceHalf U i c sigma) F) y) (HCPolySupport.euclideanGradient φ y) = ∫ (y : HCPolySupport.Vec d) in Section4.Provider.ExcessDecay.faceHalf U i c sigma, HCPolySupport.vecDot (F y) (HCPolySupport.euclideanGradient (fun (z : HCPolySupport.Vec d) => φ z - φ (HCPolySupport.coordFaceReflection c i z)) y)

The odd extension of a flux field, tested on the symmetric domain, is the original flux tested on the half against the odd fold.

2. The scalar leg

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.integral_mul_oddFaceExtend_eq {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUopen : IsOpen U) {i : Fin d} {c sigma : ℝ} (hUsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection c i y ∈ U ↔ y ∈ U) {h : HCPolySupport.Vec d → ℝ} (hh : MeasureTheory.MemLp (Section4.Provider.ExcessDecay.zeroExtend (Section4.Provider.ExcessDecay.faceHalf U i c sigma) h) 2 MeasureTheory.volume) {φ : HCPolySupport.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : ∫ (y : HCPolySupport.Vec d) in U, Section4.Provider.ExcessDecay.oddFaceExtend c i (Section4.Provider.ExcessDecay.zeroExtend (Section4.Provider.ExcessDecay.faceHalf U i c sigma) h) y * φ y = ∫ (y : HCPolySupport.Vec d) in Section4.Provider.ExcessDecay.faceHalf U i c sigma, h y * (φ y - φ (HCPolySupport.coordFaceReflection c i y))

The odd extension of a scalar source, tested on the symmetric domain, is the original source tested on the half against the odd fold.