Constant cube data

The constant H¹ cube object and its value, gradient and subtraction laws are shared by the interior Caccioppoli and zero-trace corrector routes.

1. The constant datum

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumH1 {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier

The constant function as an H¹ function of a cube.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumH1 Q c = HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain ⋯ ⋯

theorem Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumH1_toFun {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) : (constantDatumH1 Q c).toFun = fun (x : HCPolySupport.Vec d) => c

theorem Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumH1_grad {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) : (constantDatumH1 Q c).grad = fun (x : HCPolySupport.Vec d) => 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sub_constantDatumH1_grad {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) (c : ℝ) : (u - constantDatumH1 Q c).grad = u.grad

The gradient of a constant-shifted H¹ function.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sub_constantDatumH1_toFun {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) (c : ℝ) : (u - constantDatumH1 Q c).toFun = fun (y : HCPolySupport.Vec d) => u.toFun y - c

The values of a constant-shifted H¹ function.