Coarse-graining support: Support.Sobolev.W1p.WeakGradientClosure #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Finite-exponent closure of weak gradients #
This file records the finite-p graph-closure step for the concrete
coordinate weak-gradient representation. It is deliberately independent of
any zero-trace approximation: that additional closure property is supplied by
the next layer.
theorem
HCPolySupport.HasWeakPartialDerivOn.of_tendsto_eLpNorm_finiteLp
{d : ℕ}
{U : Set (Vec d)}
(p : FiniteLpExponent)
{i : Fin d}
{u gi : Vec d → ℝ}
{u_n g_n : ℕ → Vec d → ℝ}
(hu : MeasureTheory.MemLp u p.exponent (MeasureTheory.volume.restrict U))
(hgi : MeasureTheory.MemLp gi p.exponent (MeasureTheory.volume.restrict U))
(hu_n : ∀ (n : ℕ), MeasureTheory.MemLp (u_n n) p.exponent (MeasureTheory.volume.restrict U))
(hg_n : ∀ (n : ℕ), MeasureTheory.MemLp (g_n n) p.exponent (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) p.exponent (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) p.exponent (MeasureTheory.volume.restrict U))
Filter.atTop (nhds 0))
:
HasWeakPartialDerivOn U i u gi
The finite-p weak derivative graph is closed under coordinatewise
L^p convergence.
theorem
HCPolySupport.HasWeakGradientOn.of_tendsto_eLpNorm_finiteLp
{d : ℕ}
{U : Set (Vec d)}
(p : FiniteLpExponent)
{u : Vec d → ℝ}
{Du : Vec d → Vec d}
{u_n : ℕ → Vec d → ℝ}
{Du_n : ℕ → Vec d → Vec d}
(hu : MeasureTheory.MemLp u p.exponent (MeasureTheory.volume.restrict U))
(hDu : GradMemLpOn U p.exponent Du)
(hu_n : ∀ (n : ℕ), MeasureTheory.MemLp (u_n n) p.exponent (MeasureTheory.volume.restrict U))
(hDu_n : ∀ (n : ℕ), GradMemLpOn U p.exponent (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) p.exponent (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) p.exponent (MeasureTheory.volume.restrict U))
Filter.atTop (nhds 0))
:
HasWeakGradientOn U u Du
The finite-p weak-gradient graph is closed under coordinatewise L^p
convergence.