Coarse-graining support: Support.Sobolev.H1.Algebra.Membership

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.memH1_zero {d : ℕ} {U : Set (Vec d)} : MemH1 U 0

theorem HCPolySupport.memH1_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) {u : Vec d → ℝ} (hu : MemH1 U u) : MemH1 U fun (x : Vec d) => c * u x

theorem HCPolySupport.memH1_neg {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hu : MemH1 U u) : MemH1 U fun (x : Vec d) => -u x

theorem HCPolySupport.memH1_add {d : ℕ} {U : Set (Vec d)} {u v : Vec d → ℝ} (hu : MemH1 U u) (hv : MemH1 U v) : MemH1 U fun (x : Vec d) => u x + v x

theorem HCPolySupport.memH1_sub {d : ℕ} {U : Set (Vec d)} {u v : Vec d → ℝ} (hu : MemH1 U u) (hv : MemH1 U v) : MemH1 U fun (x : Vec d) => u x - v x

theorem HCPolySupport.memH10_zero {d : ℕ} {U : Set (Vec d)} : MemH10 U 0

theorem HCPolySupport.memH10_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) {u : Vec d → ℝ} (hu : MemH10 U u) : MemH10 U fun (x : Vec d) => c * u x

theorem HCPolySupport.memH10_neg {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hu : MemH10 U u) : MemH10 U fun (x : Vec d) => -u x

theorem HCPolySupport.memH10_add {d : ℕ} {U : Set (Vec d)} {u v : Vec d → ℝ} (hu : MemH10 U u) (hv : MemH10 U v) : MemH10 U fun (x : Vec d) => u x + v x

theorem HCPolySupport.memH10_sub {d : ℕ} {U : Set (Vec d)} {u v : Vec d → ℝ} (hu : MemH10 U u) (hv : MemH10 U v) : MemH10 U fun (x : Vec d) => u x - v x

theorem HCPolySupport.memH1_mul_of_contDiff_hasCompactSupport {d : ℕ} {U : Set (Vec d)} {φ u : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hu : MemH1 U u) : MemH1 U fun (x : Vec d) => φ x * u x

theorem HCPolySupport.memH10_mul_of_contDiff_hasCompactSupport {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {φ u : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) (hu : MemH1 U u) : MemH10 U fun (x : Vec d) => φ x * u x