HarmonicityTransferFace

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

The single-face harmonicity transfer

Let U be an open bounded convex domain symmetric under the reflection r in the hyperplane {yᵢ = a}, and let H = faceHalf U i a σ be one of the two open halves it cuts. If v is weakly harmonic on H, then its odd extension across the face — w = v - v ∘ r after zero extension off H — is weakly harmonic on all of U.

Scope

The H¹(U) packaging of the odd extension is an input here: the theorem takes an H1Function U whose recorded gradient is the odd extension of the zero-extended gradient of v, and proves that it is weakly harmonic. Producing that packaging from a localized zero-trace hypothesis on the met face is the separate job of the weak-gradient locality lemma (WeakGradientLocality.lean) — the harmonicity proved here never uses the zero-trace hypothesis, only the harmonicity of v on the half.

References

• CoarseGraining, Homogenization/Sobolev/Foundations/CubeReflection/ (the reflection, its measure preservation, and the even fold foldedCoordFaceTest).

1. Reflection algebra

theorem Algsuperdiff.Section4.Provider.ExcessDecay.vecDot_coordReflectionLinear_left {d : ℕ} (i : Fin d) (A B : HCPolySupport.Vec d) : HCPolySupport.vecDot ((HCPolySupport.coordReflectionLinear i) A) B = HCPolySupport.vecDot A ((HCPolySupport.coordReflectionLinear i) B)

The coordinate reflection is self-adjoint for the coordinate dot product.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coordFaceReflection_apply {d : ℕ} (a : ℝ) (i : Fin d) (y : HCPolySupport.Vec d) (j : Fin d) : HCPolySupport.coordFaceReflection a i y j = if j = i then 2 * a - y j else y j

The coordinates of the face reflection: the normal coordinate is flipped about a, the tangential ones are untouched.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coordFaceReflection_eq_self {d : ℕ} {a : ℝ} {i : Fin d} {y : HCPolySupport.Vec d} (hy : y i = a) : HCPolySupport.coordFaceReflection a i y = y

A point of the reflecting hyperplane is fixed.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.tsupport_comp_coordFaceReflection_subset {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : ℝ) (i : Fin d) (hUsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection a i y ∈ U ↔ y ∈ U) {φ : HCPolySupport.Vec d → ℝ} (hφU : tsupport φ ⊆ U) : (tsupport fun (z : HCPolySupport.Vec d) => φ (HCPolySupport.coordFaceReflection a i z)) ⊆ U

If U is invariant under the reflection, so is the closed support of any test function supported in U — hence the reflected test is again supported in U.

2. Integrability of the tested pairing

3. The transfer

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_of_oddFaceExtendGrad {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {i : Fin d} {a σ : ℝ} (hσ : |σ| = 1) (hUsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection a i y ∈ U ↔ y ∈ U) (v : HCPolySupport.H1Function (faceHalf U i a σ)) (hv : Support.IsWeaklyHarmonicOn (faceHalf U i a σ) v) (w : HCPolySupport.H1Function U) (hw : ∀ (y : HCPolySupport.Vec d), w.grad y = oddFaceExtendGrad a i (zeroExtendGrad (faceHalf U i a σ) v.grad) y) : Support.IsWeaklyHarmonicOn U w

The single-face harmonicity transfer.

U is an open bounded convex domain invariant under the reflection r in {yᵢ = a}; H = faceHalf U i a σ is the open half on the σ-side; v is weakly harmonic on H; and w is an H¹(U) function whose gradient is the odd extension of v's gradient, zero-extended off H. Then w is weakly harmonic on U.

The proof folds the test function oddly, ψ = φ - φ ∘ r, uses to make ψ an admissible H¹₀(H) competitor, and reduces the reflected half of the integral to H by the measure-preserving change of variables.