Coarse-graining support: Support.Sobolev.Foundations.PoincareW1p.ConvexApproxTendsto

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

theorem HCPolySupport.W1pFunction.unitConvexApproxScale_pos (n : ℕ) : 0 < unitConvexApproxScale n

noncomputable def HCPolySupport.W1pFunction.convexApproxSmoothW1p {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hp1 : 1 ≤ p) (u : W1pFunction U p) (x0 : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) : W1pFunction U p

The W^{1,p} smoothing of u obtained by convolving its zero extension at scale r / (n + 1) and evaluating at the affine contraction toward x0.

Equations

• HCPolySupport.W1pFunction.convexApproxSmoothW1p hU hp1 u x0 hr n = HCPolySupport.W1pFunction.ofContDiffOnIsOpenBoundedConvexDomain hU ⋯

theorem HCPolySupport.W1pFunction.tendsto_convexApproxSmoothW1p_toFun_eLpNorm_sub {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (u : W1pFunction U p) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (convexApproxSmoothW1p hU hp1 u x0 hr n).toFun x - u.toFun x) p (volumeMeasureOn U)) Filter.atTop (nhds 0)

Canonical convex smooth approximants converge to a W^{1,p} function in the value L^p norm on a bounded open convex domain.

theorem HCPolySupport.W1pFunction.tendsto_convexApproxSmoothW1p_grad_eLpNorm_sub {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (u : W1pFunction U p) {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) => (convexApproxSmoothW1p hU hp1 u x0 hr n).grad x i - u.grad x i) p (volumeMeasureOn U)) Filter.atTop (nhds 0)

Canonical convex smooth approximants converge coordinatewise to the weak gradient in the L^p norm on a bounded open convex domain.

theorem HCPolySupport.W1pFunction.tendsto_convexApproxSmoothW1p_gradientCoordLpSeminormSum {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (u : W1pFunction U p) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) : Filter.Tendsto (fun (n : ℕ) => (convexApproxSmoothW1p hU hp1 u x0 hr n).gradientCoordLpSeminormSum) Filter.atTop (nhds u.gradientCoordLpSeminormSum)

theorem HCPolySupport.W1pFunction.tendsto_convexApproxSmoothW1p_subAverageLpSeminorm_ofReal {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {q : ℝ} (hq : 1 < q) (u : W1pFunction U (ENNReal.ofReal q)) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) : Filter.Tendsto (fun (n : ℕ) => (convexApproxSmoothW1p hU ⋯ u x0 hr n).subAverageLpSeminorm) Filter.atTop (nhds u.subAverageLpSeminorm)