StepFourHarmonicWindowSeam

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

1. Weak harmonicity restricts to open subsets

theorem Algsuperdiff.Section4.Provider.Regularity.isWeaklyHarmonicOn_restrict {d : ℕ} {W V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (hVW : V ⊆ W) {v : HCPolySupport.H1Function W} (h : Support.IsWeaklyHarmonicOn W v) : Support.IsWeaklyHarmonicOn V (v.restrict hV hVW)

Weak harmonicity restricts to every open subset.

If v is weakly harmonic on W and V ⊆ W is open, the restriction of v is weakly harmonic on V: every test function of H¹₀(V) extends by zero to one of H¹₀(W).