Coarse-graining support: Support.Sobolev.H1.Algebra.H10Function

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

@[instance_reducible]

instance HCPolySupport.H10Function.instZero {d : ℕ} {U : Set (Vec d)} : Zero (H10Function U)

Equations

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

@[instance_reducible]

instance HCPolySupport.H10Function.instSMulReal {d : ℕ} {U : Set (Vec d)} : SMul ℝ (H10Function U)

Equations

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

@[instance_reducible]

instance HCPolySupport.H10Function.instNeg {d : ℕ} {U : Set (Vec d)} : Neg (H10Function U)

Equations

• HCPolySupport.H10Function.instNeg = { neg := fun (u : HCPolySupport.H10Function U) => -1 • u }

@[instance_reducible]

instance HCPolySupport.H10Function.instAdd {d : ℕ} {U : Set (Vec d)} : Add (H10Function U)

Equations

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

@[instance_reducible]

instance HCPolySupport.H10Function.instSub {d : ℕ} {U : Set (Vec d)} : Sub (H10Function U)

Equations

• HCPolySupport.H10Function.instSub = { sub := fun (u v : HCPolySupport.H10Function U) => u + -v }

noncomputable def HCPolySupport.H10Function.mulContDiffMemLpTop {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_memTop : MeasureTheory.MemLp φ ⊤ (MeasureTheory.volume.restrict U)) (hdφ_memTop : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => (fderiv ℝ φ x) (basisVec i)) ⊤ (MeasureTheory.volume.restrict U)) : H10Function U

Multiplication of an H¹₀ function by a smooth scalar multiplier which is bounded, together with its first derivatives, on the underlying domain. The approximants remain compactly supported in the domain because the original H¹₀ approximants are compactly supported there.

Equations

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

@[simp]

theorem HCPolySupport.H10Function.mulContDiffMemLpTop_toFun {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_memTop : MeasureTheory.MemLp φ ⊤ (MeasureTheory.volume.restrict U)) (hdφ_memTop : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => (fderiv ℝ φ x) (basisVec i)) ⊤ (MeasureTheory.volume.restrict U)) : (u.mulContDiffMemLpTop hφ hφ_memTop hdφ_memTop).toFun = fun (x : Vec d) => φ x * u.toFun x

@[simp]

theorem HCPolySupport.H10Function.mulContDiffMemLpTop_grad {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_memTop : MeasureTheory.MemLp φ ⊤ (MeasureTheory.volume.restrict U)) (hdφ_memTop : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => (fderiv ℝ φ x) (basisVec i)) ⊤ (MeasureTheory.volume.restrict U)) : (u.mulContDiffMemLpTop hφ hφ_memTop hdφ_memTop).grad = fun (x : Vec d) (i : Fin d) => φ x * u.grad x i + u.toFun x * (fderiv ℝ φ x) (basisVec i)

noncomputable def HCPolySupport.H10Function.mulContDiffHasCompactSupport {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : H10Function U

Multiplication of an H¹₀ function by a smooth compactly supported scalar function. Unlike mulSmoothCutoff, the multiplier itself need not be supported in the domain: the H¹₀ approximants already have support in the domain, and multiplying them by the scalar multiplier preserves that support.

Equations

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

@[simp]

theorem HCPolySupport.H10Function.mulContDiffHasCompactSupport_toFun {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : (u.mulContDiffHasCompactSupport hφ hφ_compact).toFun = fun (x : Vec d) => φ x * u.toFun x

noncomputable def HCPolySupport.H10Function.mulSmoothCutoff {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {φ : Vec d → ℝ} (hU : IsOpen U) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) : H10Function U

The product of a zero-trace H¹ function with a smooth compactly supported cutoff whose topological support lies in U.

Equations

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

@[simp]

theorem HCPolySupport.H10Function.mulSmoothCutoff_toFun {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {φ : Vec d → ℝ} (hU : IsOpen U) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) : (u.mulSmoothCutoff hU hφ hφ_compact hφ_sub).toFun = fun (x : Vec d) => φ x * u.toFun x