Coarse-graining support: Support.Sobolev.CubeEmbedding.FoldExtensionFiniteP #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Finite-p even-fold extension on an axis box #
The W^{1,p} companion to foldExtension. Smooth convex-domain
approximants are cut off outside the tripled box, transported by the fold, and
closed using finite-exponent Hölder pairings against compactly supported test
functions.
theorem
HCPolySupport.tendsto_eLpNorm_convexApproxSmoothW1p
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
(p : FiniteLpExponent)
(u : W1pFunction U p.exponent)
{x0 : Vec d}
{r : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 < r)
:
Filter.Tendsto
(fun (n : ℕ) =>
MeasureTheory.eLpNorm (fun (x : Vec d) => (W1pFunction.convexApproxSmoothW1p hU ⋯ u x0 hr n).toFun x - u.toFun x)
p.exponent (MeasureTheory.volume.restrict U))
Filter.atTop (nhds 0)
theorem
HCPolySupport.tendsto_eLpNorm_grad_convexApproxSmoothW1p
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
(p : FiniteLpExponent)
(u : W1pFunction U p.exponent)
{x0 : Vec d}
{r : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 < r)
(i : Fin d)
:
Filter.Tendsto
(fun (n : ℕ) =>
MeasureTheory.eLpNorm (fun (x : Vec d) => (W1pFunction.convexApproxSmoothW1p hU ⋯ u x0 hr n).grad x i - u.grad x i)
p.exponent (MeasureTheory.volume.restrict U))
Filter.atTop (nhds 0)
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
structure
HCPolySupport.FoldExtensionFiniteP
{d : ℕ}
(lo hi : Vec d)
(p : FiniteLpExponent)
(u : W1pFunction (Box lo hi) p.exponent)
:
Data of the finite-p even-fold extension.
- Eu : W1pFunction (Box3 lo hi) p.exponent
The Sobolev extension to the enlarged box, agreeing a.e. with
uand its weak gradient on the original box. - eLpNorm_le : MeasureTheory.eLpNorm self.Eu.toFun p.exponent (MeasureTheory.volume.restrict (Box3 lo hi)) ≤ (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm u.toFun p.exponent (MeasureTheory.volume.restrict (Box lo hi))