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

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

theorem HCPolySupport.memLpOn_mono {d : ℕ} {U V : Set (Vec d)} {p : ENNReal} {u : Vec d → ℝ} (hVU : V ⊆ U) (hu : MemLpOn U p u) : MemLpOn V p u

theorem HCPolySupport.gradMemLpOn_mono {d : ℕ} {U V : Set (Vec d)} {p : ENNReal} {Du : Vec d → Vec d} (hVU : V ⊆ U) (hDu : GradMemLpOn U p Du) : GradMemLpOn V p Du

theorem HCPolySupport.HasWeakPartialDerivOn.restrict {d : ℕ} {U V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) {i : Fin d} {u gi : Vec d → ℝ} (h : HasWeakPartialDerivOn U i u gi) : HasWeakPartialDerivOn V i u gi

theorem HCPolySupport.HasWeakGradientOn.restrict {d : ℕ} {U V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) {u : Vec d → ℝ} {Du : Vec d → Vec d} (h : HasWeakGradientOn U u Du) : HasWeakGradientOn V u Du

theorem HCPolySupport.HasWeakPartialDerivOn.of_contDiff {d : ℕ} {U : Set (Vec d)} {i : Fin d} {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : HasWeakPartialDerivOn U i f fun (x : Vec d) => (fderiv ℝ f x) (basisVec i)

theorem HCPolySupport.HasWeakGradientOn.of_contDiff {d : ℕ} {U : Set (Vec d)} {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : HasWeakGradientOn U f fun (x : Vec d) (i : Fin d) => (fderiv ℝ f x) (basisVec i)

theorem HCPolySupport.W1pFunction.ext {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {u v : W1pFunction U p} (htoFun : u.toFun = v.toFun) (hgrad : u.grad = v.grad) : u = v

theorem HCPolySupport.W1pFunction.ext_iff {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {u v : W1pFunction U p} : u = v ↔ u.toFun = v.toFun ∧ u.grad = v.grad

theorem HCPolySupport.W1pFunction.hasWeakPartialDerivOn {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (i : Fin d) : HasWeakPartialDerivOn U i u.toFun fun (x : Vec d) => u.grad x i

theorem HCPolySupport.W1pFunction.grad_memLp {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (i : Fin d) : MemLpOn U p fun (x : Vec d) => u.grad x i

theorem HCPolySupport.W1pFunction.memW1p {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : MemW1p U p u.toFun

noncomputable def HCPolySupport.W1pFunction.ofContDiff {d : ℕ} {U : Set (Vec d)} (_hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) (hf_supp : HasCompactSupport f) (p : ENNReal) : W1pFunction U p

A compactly supported C¹ function viewed as a W^{1,p} function on U, with its classical coordinate derivatives as weak gradient.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.W1pFunction.ofContDiffOnIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsSobolevRegularDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : W1pFunction U p

Package a globally smooth function as a W^{1,p}(U) witness on a bounded measurable domain. Unlike ofContDiff, this constructor does not require compact support, because boundedness of U gives the needed L^p control on the restriction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.W1pFunction.ofContDiffOnIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : W1pFunction U p

Bounded open convex domains admit the bounded-domain smooth constructor for W^{1,p}.

Equations

• HCPolySupport.W1pFunction.ofContDiffOnIsOpenBoundedConvexDomain hU hf = HCPolySupport.W1pFunction.ofContDiffOnIsSobolevRegularDomain ⋯ hf

def HCPolySupport.W1pFunction.restrict {d : ℕ} {U V : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (hVopen : IsOpen V) (hVU : V ⊆ U) : W1pFunction V p

Restriction of a W^{1,p} witness to an open subset, retaining its value and weak-gradient representatives.

Equations

• u.restrict hVopen hVU = { toFun := u.toFun, grad := u.grad, memLp := ⋯, gradMemLp := ⋯, hasWeakGradient := ⋯ }

def HCPolySupport.W1pFunction.toW10pFunction {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (happrox : u.SupportedSmoothApproximation) : W10pFunction U p

Upgrade a W^{1,p} witness to W^{1,p}_0 from an explicit supported smooth approximation package. This is the final zero-trace packaging target: the support data is an input, not a consequence of domain convexity alone.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.W1pFunction.memW10p_of_supportedSmoothApproximation {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (happrox : u.SupportedSmoothApproximation) : MemW10p U p u.toFun

theorem HCPolySupport.W1pFunction.memW10p_of_hasSupportedSmoothApproximation {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (happrox : u.HasSupportedSmoothApproximation) : MemW10p U p u.toFun

theorem HCPolySupport.W10pFunction.memW1p {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W10pFunction U p) : MemW1p U p u.toFun

noncomputable def HCPolySupport.W10pFunction.ofContDiff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (hf_sub : tsupport f ⊆ U) (p : ENNReal) : W10pFunction U p

A smooth function with compact topological support in U, viewed in W^{1,p}_0 using its constant approximation sequence.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.W10pFunction.memW10p {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W10pFunction U p) : MemW10p U p u.toFun

def HCPolySupport.W10pFunction.supportedSmoothApproximation {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W10pFunction U p) : u.SupportedSmoothApproximation

Every bundled W10pFunction exposes its supported smooth approximation data for the underlying W1pFunction.

Equations

• u.supportedSmoothApproximation = { approx := u.approx, approx_smooth := ⋯, approx_hasCompactSupport := ⋯, approx_support_subset := ⋯, tendsto_approx := ⋯, tendsto_approx_grad := ⋯ }

theorem HCPolySupport.W10pFunction.hasSupportedSmoothApproximation {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W10pFunction U p) : u.HasSupportedSmoothApproximation

theorem HCPolySupport.memW1p_of_memW10p {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {u : Vec d → ℝ} (hu : MemW10p U p u) : MemW1p U p u

theorem HCPolySupport.memW1p_of_contDiffOnIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsSobolevRegularDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : MemW1p U p f

theorem HCPolySupport.memW1p_of_contDiffOnIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : MemW1p U p f

theorem HCPolySupport.memW1p_restrict {d : ℕ} {U V : Set (Vec d)} {p : ENNReal} {u : Vec d → ℝ} (hVopen : IsOpen V) (hVU : V ⊆ U) (hu : MemW1p U p u) : MemW1p V p u