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

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

H¹(U) is modeled here by explicit witnesses: a function, a candidate weak gradient, L² control on both, and the integration-by-parts identity against smooth compactly supported tests. H¹₀(U) adds the usual approximation package by smooth compactly supported functions supported in U.

@[reducible, inline]

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

Square-integrability with respect to Lebesgue measure restricted to U.

Equations

• HCPolySupport.MemL2On U u = MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict U)

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

Square-integrability on U of every coordinate of the supplied gradient field.

Equations

• HCPolySupport.GradMemL2On U Du = ∀ (i : Fin d), HCPolySupport.MemL2On U fun (x : HCPolySupport.Vec d) => Du x i

structure HCPolySupport.H1Function {d : ℕ} (U : Set (Vec d)) : Type

A scalar function and weak gradient whose components are square-integrable on U.

• toFun : Vec d → ℝ

  The pointwise scalar representative of the Sobolev function.

• grad : Vec d → Vec d

  The pointwise weak gradient, with square-integrable coordinates on U.

• memL2 : MemL2On U self.toFun
• gradMemL2 : GradMemL2On U self.grad
• hasWeakGradient : HasWeakGradientOn U self.toFun self.grad

@[instance_reducible]

instance HCPolySupport.instCoeFunH1FunctionForallVecReal {d : ℕ} {U : Set (Vec d)} : CoeFun (H1Function U) fun (x : H1Function U) => Vec d → ℝ

Equations

• HCPolySupport.instCoeFunH1FunctionForallVecReal = { coe := fun (u : HCPolySupport.H1Function U) => u.toFun }

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

Existence of an H¹ representative on U equal to the given function.

Equations

• HCPolySupport.MemH1 U u = ∃ (v : HCPolySupport.H1Function U), v.toFun = u

structure HCPolySupport.H10Function {d : ℕ} (U : Set (Vec d)) extends HCPolySupport.H1Function U : Type

An H¹ function approximated in value and gradient by smooth functions compactly supported in U.

• toFun : Vec d → ℝ
• grad : Vec d → Vec d
• memL2 : MemL2On U self.toFun
• gradMemL2 : GradMemL2On U self.grad
• hasWeakGradient : HasWeakGradientOn U self.toFun self.grad
• approx : ℕ → Vec d → ℝ

  The smooth compactly supported sequence converging in H¹ on 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) 2 (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) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)

@[instance_reducible]

instance HCPolySupport.instCoeFunH10FunctionForallVecReal {d : ℕ} {U : Set (Vec d)} : CoeFun (H10Function U) fun (x : H10Function U) => Vec d → ℝ

Equations

• HCPolySupport.instCoeFunH10FunctionForallVecReal = { coe := fun (u : HCPolySupport.H10Function U) => u.toFun }

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

Existence of an H¹₀ representative on U equal to the given function.

Equations

• HCPolySupport.MemH10 U u = ∃ (v : HCPolySupport.H10Function U), v.toFun = u

noncomputable def HCPolySupport.MeanZeroOn {d : ℕ} (U : Set (Vec d)) (u : Vec d → ℝ) : Prop

Vanishing of the function's Lebesgue integral over U.

Equations

• HCPolySupport.MeanZeroOn U u = (∫ (x : HCPolySupport.Vec d) in U, u x = 0)