OddReflectionAssembly

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

The odd reflection on the §4.3 windows: the one-met-face transfer

The abstract single-face transfer of HarmonicityTransferFace.lean is stated for an arbitrary reflection-symmetric open bounded convex domain.

The two geometric facts

• faceHalf_reflectedWindow_of_meetsUpperFace (and its lower-face twin) — the half of the reflected window on the window side of the met face is the truncated window itself.
• mem_reflectedWindow_coordFaceReflection_iff — the reflected window is invariant under the reflection in the met face. This one needs only k < m and the met face itself: the reflected edge (windowLo, 3^m - windowLo) is symmetric about (1/2)·3^m because its two endpoints sum to 3^m.

The transfer

isWeaklyHarmonicOn_reflectedWindow_of_meetsUpperFace composes them with the abstract theorem: a weakly harmonic v on the truncated window has weakly harmonic odd extension on the reflected window. As in the abstract statement, the H¹(reflectedWindow) packaging of the odd extension is an input.

Scope note (measured, not hidden)

Only the one-met-face regime is closed here.

1. Transporting an H¹ datum along an equality of domains

def Algsuperdiff.Section4.Provider.ExcessDecay.h1FunctionOfSetEq {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (h : U = V) (u : HCPolySupport.H1Function U) : HCPolySupport.H1Function V

Transport of an H¹ function along an equality of its domain.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.h1FunctionOfSetEq h u = h ▸ u

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h1FunctionOfSetEq_grad {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (h : U = V) (u : HCPolySupport.H1Function U) : (h1FunctionOfSetEq h u).grad = u.grad

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_h1FunctionOfSetEq {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (h : U = V) {u : HCPolySupport.H1Function U} (hu : Support.IsWeaklyHarmonicOn U u) : Support.IsWeaklyHarmonicOn V (h1FunctionOfSetEq h u)

2. The met-face geometry of the reflected window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceHalf_reflectedWindow_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hup : MeetsUpperFace x m k i) (hother : ∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m k j ∧ ¬MeetsLowerFace x m k j) : faceHalf (reflectedWindow x m k) i (1 / 2 * 3 ^ m) 1 = truncatedWindow x m k

The window is the half of its reflection. If the upper i-face of ∂□_m is the only met face, the half of reflectedWindow x m k on the window side of that face is exactly the truncated window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceHalf_reflectedWindow_of_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hlow : MeetsLowerFace x m k i) (hother : ∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m k j ∧ ¬MeetsLowerFace x m k j) : faceHalf (reflectedWindow x m k) i (-(1 / 2) * 3 ^ m) (-1) = truncatedWindow x m k

The lower-face twin of faceHalf_reflectedWindow_of_meetsUpperFace.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_reflectedWindow_coordFaceReflection_iff {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hup : MeetsUpperFace x m k i) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i y ∈ reflectedWindow x m k ↔ y ∈ reflectedWindow x m k

The reflected window is symmetric in a met upper face. Only k < m and the met face itself are needed: the reflected i-edge has endpoints summing to 3^m = 2·((1/2)·3^m).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_reflectedWindow_coordFaceReflection_iff_lower {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hlow : MeetsLowerFace x m k i) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i y ∈ reflectedWindow x m k ↔ y ∈ reflectedWindow x m k

The lower-face twin of mem_reflectedWindow_coordFaceReflection_iff.

3. The one-met-face harmonicity transfer on the windows

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_reflectedWindow_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hup : MeetsUpperFace x m k i) (hother : ∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m k j ∧ ¬MeetsLowerFace x m k j) (v : HCPolySupport.H1Function (truncatedWindow x m k)) (hv : Support.IsWeaklyHarmonicOn (truncatedWindow x m k) v) (w : HCPolySupport.H1Function (reflectedWindow x m k)) (hw : ∀ (y : HCPolySupport.Vec d), w.grad y = oddFaceExtendGrad (1 / 2 * 3 ^ m) i (zeroExtendGrad (truncatedWindow x m k) v.grad) y) : Support.IsWeaklyHarmonicOn (reflectedWindow x m k) w

The one-met-face transfer, upper face.

V = (x + □_k) ∩ □_m meets exactly one face of ∂□_m, the upper i-face. If v is weakly harmonic on V and w is an H¹ function of the reflected window whose gradient is the odd extension of v's across that face, then w is weakly harmonic on the reflected window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_reflectedWindow_of_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hlow : MeetsLowerFace x m k i) (hother : ∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m k j ∧ ¬MeetsLowerFace x m k j) (v : HCPolySupport.H1Function (truncatedWindow x m k)) (hv : Support.IsWeaklyHarmonicOn (truncatedWindow x m k) v) (w : HCPolySupport.H1Function (reflectedWindow x m k)) (hw : ∀ (y : HCPolySupport.Vec d), w.grad y = oddFaceExtendGrad (-(1 / 2) * 3 ^ m) i (zeroExtendGrad (truncatedWindow x m k) v.grad) y) : Support.IsWeaklyHarmonicOn (reflectedWindow x m k) w

The one-met-face transfer, lower face.