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

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

W^{1,p}(U) and W^{1,p}_0(U) witnesses parallel the existing H¹ encoding but keep the exponent p explicit.

@[reducible, inline]

abbrev HCPolySupport.MemLpOn {d : ℕ} (U : Set (Vec d)) (p : ENNReal) (u : Vec d → ℝ) : Prop

Membership in Lᵖ for Lebesgue measure restricted to U.

Equations

• HCPolySupport.MemLpOn U p u = MeasureTheory.MemLp u p (MeasureTheory.volume.restrict U)

def HCPolySupport.GradMemLpOn {d : ℕ} (U : Set (Vec d)) (p : ENNReal) (Du : Vec d → Vec d) : Prop

Membership in Lᵖ(U) of every coordinate of the supplied gradient field.

Equations

• HCPolySupport.GradMemLpOn U p Du = ∀ (i : Fin d), HCPolySupport.MemLpOn U p fun (x : HCPolySupport.Vec d) => Du x i

structure HCPolySupport.W1pFunction {d : ℕ} (U : Set (Vec d)) (p : ENNReal) : Type

A scalar function and weak gradient with value and gradient coordinates in Lᵖ(U).

• toFun : Vec d → ℝ

  The pointwise scalar representative of the Sobolev function.

• grad : Vec d → Vec d

  The pointwise weak gradient, with coordinates in Lᵖ(U).

• memLp : MemLpOn U p self.toFun
• gradMemLp : GradMemLpOn U p self.grad
• hasWeakGradient : HasWeakGradientOn U self.toFun self.grad

@[instance_reducible]

instance HCPolySupport.instCoeFunW1pFunctionForallVecReal {d : ℕ} {U : Set (Vec d)} {p : ENNReal} : CoeFun (W1pFunction U p) fun (x : W1pFunction U p) => Vec d → ℝ

Equations

• HCPolySupport.instCoeFunW1pFunctionForallVecReal = { coe := fun (u : HCPolySupport.W1pFunction U p) => u.toFun }

def HCPolySupport.MemW1p {d : ℕ} (U : Set (Vec d)) (p : ENNReal) (u : Vec d → ℝ) : Prop

Existence of a W¹ᵖ representative on U equal to the given function.

Equations

• HCPolySupport.MemW1p U p u = ∃ (v : HCPolySupport.W1pFunction U p), v.toFun = u

structure HCPolySupport.W1pFunction.SupportedSmoothApproximation {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : Type

The exact supported smooth approximation data needed to upgrade a W1pFunction witness to W10pFunction.

This is intentionally a separate zero-trace hypothesis: bounded open convexity gives a natural smooth approximation mechanism for bare W^{1,p} functions, but it does not imply compactly supported approximation inside U for every Sobolev function.

• approx : ℕ → Vec d → ℝ

  The smooth sequence supported compactly in U and converging in value and gradient in Lᵖ.

• approx_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (self.approx n)
• approx_hasCompactSupport (n : ℕ) : HasCompactSupport (self.approx n)
• approx_support_subset (n : ℕ) : tsupport (self.approx n) ⊆ U
• tendsto_approx : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => self.approx n x - u.toFun x) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
• tendsto_approx_grad (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (self.approx n) x) (basisVec i) - u.grad x i) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)

def HCPolySupport.W1pFunction.HasSupportedSmoothApproximation {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : Prop

Proposition-valued form of SupportedSmoothApproximation, useful when the actual approximating sequence should remain hidden.

Equations

• u.HasSupportedSmoothApproximation = Nonempty u.SupportedSmoothApproximation

structure HCPolySupport.W10pFunction {d : ℕ} (U : Set (Vec d)) (p : ENNReal) extends HCPolySupport.W1pFunction U p : Type

A W¹ᵖ function approximated in value and gradient by smooth functions compactly supported in U.

• toFun : Vec d → ℝ
• grad : Vec d → Vec d
• memLp : MemLpOn U p self.toFun
• gradMemLp : GradMemLpOn U p self.grad
• hasWeakGradient : HasWeakGradientOn U self.toFun self.grad
• approx : ℕ → Vec d → ℝ

  The smooth compactly supported sequence converging in value and gradient in Lᵖ(U).

• approx_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (self.approx n)
• approx_hasCompactSupport (n : ℕ) : HasCompactSupport (self.approx n)
• approx_support_subset (n : ℕ) : tsupport (self.approx n) ⊆ U
• tendsto_approx : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => self.approx n x - self.toFun x) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
• tendsto_approx_grad (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (self.approx n) x) (basisVec i) - self.grad x i) p (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)

@[instance_reducible]

instance HCPolySupport.instCoeFunW10pFunctionForallVecReal {d : ℕ} {U : Set (Vec d)} {p : ENNReal} : CoeFun (W10pFunction U p) fun (x : W10pFunction U p) => Vec d → ℝ

Equations

• HCPolySupport.instCoeFunW10pFunctionForallVecReal = { coe := fun (u : HCPolySupport.W10pFunction U p) => u.toFun }

def HCPolySupport.MemW10p {d : ℕ} (U : Set (Vec d)) (p : ENNReal) (u : Vec d → ℝ) : Prop

Existence of a W¹ᵖ₀ representative on U equal to the given function.

Equations

• HCPolySupport.MemW10p U p u = ∃ (v : HCPolySupport.W10pFunction U p), v.toFun = u