Coarse-graining support: Support.Sobolev.Truncation.WeakGradientLimit

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

Weak partial derivatives are closed under L² limits

If uₙ → u and gₙ → gᵢ in L²(U) and each uₙ has weak i-partial derivative gₙ, then u has weak i-partial derivative gᵢ. The pairing identity ∫ uₙ ∂ᵢφ = −∫ gₙ φ holds for each n; both sides are continuous in the L² factor, so the identity passes to the limit.

Two spellings of the same principle are provided:

• one built on the Lebesgue L² realizations MemScalarL2 / toScalarL2 and volumeMeasureOn U, with an L² dominated-convergence helper (hasWeakPartialDerivOn_of_tendsto_L2);
• one built directly on MemLp _ 2 (volume.restrict U) via a Cauchy–Schwarz/Hölder pairing-continuity lemma, closing over both the partial derivative (HasWeakPartialDerivOn.of_tendsto_eLpNorm_two) and the full gradient (HasWeakGradientOn.of_tendsto_eLpNorm_two).

theorem HCPolySupport.tendsto_eLpNorm_two_of_tendsto_ae_of_dominated {d : ℕ} {μ : MeasureTheory.Measure (Vec d)} {f : ℕ → Vec d → ℝ} {g h : Vec d → ℝ} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hg : MeasureTheory.MemLp g 2 μ) (hh : MeasureTheory.MemLp h 2 μ) (hbound : ∀ (n : ℕ), ∀ᵐ (x : Vec d) ∂μ, ‖f n x‖ ≤ h x) (hfg : ∀ᵐ (x : Vec d) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => f n x - g x) 2 μ) Filter.atTop (nhds 0)

L² dominated convergence. If fₙ → g a.e., all dominated in norm by a fixed L² function h, with g ∈ L², then fₙ → g in L². (General finite/σ-finite measure; the dominator provides the integrability.)

theorem HCPolySupport.hasWeakPartialDerivOn_of_tendsto_L2 {d : ℕ} {U : Set (Vec d)} {i : Fin d} {u gi : Vec d → ℝ} {un gn : ℕ → Vec d → ℝ} (hu : MemScalarL2 U u) (hgi : MemScalarL2 U gi) (hun : ∀ (n : ℕ), MemScalarL2 U (un n)) (hgn : ∀ (n : ℕ), MemScalarL2 U (gn n)) (hweak : ∀ (n : ℕ), HasWeakPartialDerivOn U i (un n) (gn n)) (hun_to : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => un n x - u x) 2 (volumeMeasureOn U)) Filter.atTop (nhds 0)) (hgn_to : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => gn n x - gi x) 2 (volumeMeasureOn U)) Filter.atTop (nhds 0)) : HasWeakPartialDerivOn U i u gi

Weak partial derivative closed under L² limits. If uₙ → u and gₙ → gᵢ in L²(U), all in L²(U), and each uₙ has weak i-partial derivative gₙ, then u has weak i-partial derivative gᵢ.

theorem HCPolySupport.tendsto_setIntegral_mul_of_tendsto_eLpNorm_two {d : ℕ} {U : Set (Vec d)} {h : Vec d → ℝ} {f : ℕ → Vec d → ℝ} {g : Vec d → ℝ} (hh : MeasureTheory.MemLp h 2 (MeasureTheory.volume.restrict U)) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 (MeasureTheory.volume.restrict U)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict U)) (htend : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => f n x - g x) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Vec d) in U, f n x * h x) Filter.atTop (nhds (∫ (x : Vec d) in U, g x * h x))

Pairing against a fixed L² test is continuous along L²-convergent sequences: if f n → g in L²(U) and h ∈ L²(U), then ∫_U (f n)·h → ∫_U g·h.

theorem HCPolySupport.HasWeakPartialDerivOn.of_tendsto_eLpNorm_two {d : ℕ} {U : Set (Vec d)} {i : Fin d} {u gi : Vec d → ℝ} {u_n g_n : ℕ → Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict U)) (hgi : MeasureTheory.MemLp gi 2 (MeasureTheory.volume.restrict U)) (hu_n : ∀ (n : ℕ), MeasureTheory.MemLp (u_n n) 2 (MeasureTheory.volume.restrict U)) (hg_n : ∀ (n : ℕ), MeasureTheory.MemLp (g_n n) 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (n : ℕ), HasWeakPartialDerivOn U i (u_n n) (g_n n)) (htend_u : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => u_n n x - u x) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) (htend_g : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => g_n n x - gi x) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) : HasWeakPartialDerivOn U i u gi

Weak partial derivatives are closed under L² limits. If u n → u and g n → g in L²(U) and each u n has weak i-th partial derivative g n on U, then u has weak i-th partial derivative g.

theorem HCPolySupport.HasWeakGradientOn.of_tendsto_eLpNorm_two {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} {Du : Vec d → Vec d} {u_n : ℕ → Vec d → ℝ} {Du_n : ℕ → Vec d → Vec d} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict U)) (hDu : GradMemL2On U Du) (hu_n : ∀ (n : ℕ), MeasureTheory.MemLp (u_n n) 2 (MeasureTheory.volume.restrict U)) (hDu_n : ∀ (n : ℕ), GradMemL2On U (Du_n n)) (hweak : ∀ (n : ℕ), HasWeakGradientOn U (u_n n) (Du_n n)) (htend_u : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => u_n n x - u x) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) (htend_Du : ∀ (i : Fin d), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => Du_n n x i - Du x i) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) : HasWeakGradientOn U u Du

Weak gradients are closed under L² limits (all coordinates at once).