Coarse-graining support: Support.Sobolev.Foundations.H1Graph.Preliminaries

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

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

Smooth compactly supported test functions used to encode the weak-gradient constraints inside the L²(U) × L²(U; ℝᵈ) ambient product.

• toFun : Vec d → ℝ

  The smooth scalar test function with compact topological support contained in U.

• smooth : ContDiff ℝ (↑⊤) self.toFun
• compactSupport : HasCompactSupport self.toFun
• support_subset : tsupport self.toFun ⊆ U

@[instance_reducible]

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

Equations

• HCPolySupport.H1WeakTestFunction.instCoeFunForallVecReal = { coe := fun (φ : HCPolySupport.H1WeakTestFunction U) => φ.toFun }

noncomputable def HCPolySupport.H1WeakTestFunction.deriv {d : ℕ} {U : Set (Vec d)} (φ : H1WeakTestFunction U) (i : Fin d) : Vec d → ℝ

The ith classical derivative of a test function.

Equations

• φ.deriv i x = (fderiv ℝ φ.toFun x) (HCPolySupport.basisVec i)

theorem HCPolySupport.H1WeakTestFunction.memScalarL2 {d : ℕ} {U : Set (Vec d)} (φ : H1WeakTestFunction U) : MemScalarL2 U φ.toFun

theorem HCPolySupport.H1WeakTestFunction.deriv_memScalarL2 {d : ℕ} {U : Set (Vec d)} (φ : H1WeakTestFunction U) (i : Fin d) : MemScalarL2 U (φ.deriv i)

noncomputable def HCPolySupport.H1WeakTestFunction.toScalarL2 {d : ℕ} {U : Set (Vec d)} (φ : H1WeakTestFunction U) : ↥(ScalarL2 U)

The scalar L²(U) class of a test function.

Equations

• φ.toScalarL2 = HCPolySupport.toScalarL2 ⋯

noncomputable def HCPolySupport.H1WeakTestFunction.derivToScalarL2 {d : ℕ} {U : Set (Vec d)} (φ : H1WeakTestFunction U) (i : Fin d) : ↥(ScalarL2 U)

The scalar L²(U) class of the ith derivative of a test function.

Equations

• φ.derivToScalarL2 i = HCPolySupport.toScalarL2 ⋯

@[simp]

theorem HCPolySupport.H1WeakTestFunction.coeFn_toScalarL2 {d : ℕ} {U : Set (Vec d)} (φ : H1WeakTestFunction U) : ↑↑φ.toScalarL2 =ᵐ[volumeMeasureOn U] φ.toFun

@[simp]

theorem HCPolySupport.H1WeakTestFunction.coeFn_derivToScalarL2 {d : ℕ} {U : Set (Vec d)} (φ : H1WeakTestFunction U) (i : Fin d) : ↑↑(φ.derivToScalarL2 i) =ᵐ[volumeMeasureOn U] φ.deriv i

noncomputable def HCPolySupport.hilbertVectorCoordToScalarL2 {d : ℕ} {U : Set (Vec d)} (i : Fin d) : ↥(HilbertVectorL2 U) →L[ℝ] ↥(ScalarL2 U)

Extract the ith scalar coordinate of a Hilbert-vector L² field.

Equations

• HCPolySupport.hilbertVectorCoordToScalarL2 i = ContinuousLinearMap.compLpL 2 (HCPolySupport.volumeMeasureOn U) (ContinuousLinearMap.proj i) ∘SL HCPolySupport.hilbertVectorL2ToVectorL2

@[simp]

theorem HCPolySupport.coeFn_hilbertVectorCoordToScalarL2 {d : ℕ} {U : Set (Vec d)} (i : Fin d) (g : ↥(HilbertVectorL2 U)) : ↑↑((hilbertVectorCoordToScalarL2 i) g) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (↑↑g x).ofLp i

theorem HCPolySupport.scalarInner_eq_integral {d : ℕ} {U : Set (Vec d)} (f g : ↥(ScalarL2 U)) : inner ℝ f g = ∫ (x : Vec d) in U, ↑↑f x * ↑↑g x

theorem HCPolySupport.coordInner_eq_integral {d : ℕ} {U : Set (Vec d)} (i : Fin d) (g : ↥(HilbertVectorL2 U)) (φ : H1WeakTestFunction U) : inner ℝ ((hilbertVectorCoordToScalarL2 i) g) φ.toScalarL2 = ∫ (x : Vec d) in U, (↑↑g x).ofLp i * φ.toFun x