Coarse-graining support: Support.Sobolev.W1p.H1GradientUpgrade

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

Upgrading H¹ witnesses from higher-integrable gradients

On a bounded open convex domain, an H1Function whose weak-gradient coordinates belong to a finite L^p space is also a W^{1,p} witness. The value membership is obtained from mixed-exponent convex smoothing and the finite-p Poincare estimate; it is not an additional hypothesis.

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

noncomputable def HCPolySupport.H1Function.convexApproxSmoothH1W1p {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (p : FiniteLpExponent) (x0 : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) : W1pFunction U p.exponent

The convex smoothing of an H¹ function at scale r / (n + 1), viewed as a W^{1,p} function on the bounded open convex domain.

Equations

• HCPolySupport.H1Function.convexApproxSmoothH1W1p hU u p x0 hr n = HCPolySupport.W1pFunction.ofContDiffOnIsOpenBoundedConvexDomain hU ⋯

theorem HCPolySupport.H1Function.memLp_of_gradMemLp_on_isOpenBoundedConvexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) : MemLpOn U p.exponent u.toFun

noncomputable def HCPolySupport.H1Function.toW1pOfGradMemLp {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) : W1pFunction U p.exponent

Upgrade an H¹ witness on a bounded open convex domain to W^{1,p} when its weak-gradient coordinates have finite L^p control. The value L^p membership is derived from convex smoothing and Poincaré, and the function and weak-gradient representatives are preserved exactly.

Equations

• HCPolySupport.H1Function.toW1pOfGradMemLp hU u p hgrad = { toFun := u.toFun, grad := u.grad, memLp := ⋯, gradMemLp := hgrad, hasWeakGradient := ⋯ }

@[simp]

theorem HCPolySupport.H1Function.toW1pOfGradMemLp_toFun {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) : (toW1pOfGradMemLp hU u p hgrad).toFun = u.toFun

@[simp]

theorem HCPolySupport.H1Function.toW1pOfGradMemLp_grad {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) : (toW1pOfGradMemLp hU u p hgrad).grad = u.grad