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 Homogenization.MemL2On {d : ℕ} (U : Set (Vec d)) (u : Vec d → ℝ) : Prop

Square integrability with respect to Lebesgue measure restricted to a domain.

Equations

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

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

Coordinatewise square integrability of a gradient field on a domain.

Equations

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

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

Square-integrable scalar function equipped with a square-integrable weak gradient.

• toFun : Vec d → ℝ

  Scalar representative of the H¹ function.

• grad : Vec d → Vec d

  Coordinate weak gradient of the H¹ function.

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

@[instance_reducible]

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

Equations

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

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

Membership in H¹ expressed by existence of a bundled function with the same representative.

Equations

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

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

H¹ function approximable by smooth functions compactly supported inside the domain.

• 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 → ℝ

  Smooth compactly supported approximating sequence for the zero-boundary Sobolev function.

• 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 Homogenization.instCoeFunH10FunctionForallVecReal {d : ℕ} {U : Set (Vec d)} : CoeFun (H10Function U) fun (x : H10Function U) => Vec d → ℝ

Equations

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

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

Membership in H¹₀ expressed by existence of a bundled zero-boundary Sobolev function.

Equations

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

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

Vanishing Lebesgue integral over the specified domain.

Equations

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