H10Limit

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

H¹₀ is closed under H¹ limits

memH10_of_tendsto_H1: if f : H¹(U) is the L² limit (function and every gradient coordinate) of a sequence Fₙ of H¹(U) functions each lying in H¹₀(U), then f ∈ H¹₀(U).

Each MemH10 U Fₙ supplies an H¹₀ witness Wₙ bundling smooth compactly supported approximants Wₙ.approx k (support ⊆ U) converging in L² to Wₙ.toFun = Fₙ.toFun and to Wₙ.grad. A diagonal choice picks kₙ with all d+1 distances below 1/(n+1); the resulting ψₙ := Wₙ.approx kₙ is smooth, compactly supported in U, and converges to f and ∇f. Weak-gradient uniqueness bridges Wₙ.grad and Fₙ.grad, which agree a.e.

theorem HCPolySupport.eLpNorm_sub_swap {d : ℕ} {μ : MeasureTheory.Measure (Vec d)} (a b : Vec d → ℝ) {p : ENNReal} : MeasureTheory.eLpNorm (fun (x : Vec d) => a x - b x) p μ = MeasureTheory.eLpNorm (fun (x : Vec d) => b x - a x) p μ

Commuting eLpNorm of a pointwise difference of two functions.

theorem HCPolySupport.memH10_of_tendsto_H1 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (f : H1Function U) (F : ℕ → H1Function U) (hmem : ∀ (n : ℕ), MemH10 U (F n).toFun) (hfun : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => f.toFun x - (F n).toFun x) 2 (volumeMeasureOn U)) Filter.atTop (nhds 0)) (hgrad : ∀ (i : Fin d), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => f.grad x i - (F n).grad x i) 2 (volumeMeasureOn U)) Filter.atTop (nhds 0)) : MemH10 U f.toFun

H¹₀(U) closed under L² limits. It is closed under L² limits of the function together with all its gradient coordinates.