High-contrast homogenization: Provider.Regularity.CenteredCubeDirichletEuclideanHsDifference

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Difference stability for identity Dirichlet regularity

This module packages negation and subtraction on physical centered-cube Euclidean L2 fields, then applies identity Dirichlet regularity to the difference of two weak solutions. Neither solution gradient is assumed to belong to the positive fractional carrier.

noncomputable def HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldNeg {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : CenteredCubeEuclideanL2Field d m

Pointwise negation, packaged as a centered-cube Euclidean L2 field.

Equations

• HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldNeg F = { toField := fun (x : HCPolySupport.Vec d) => -F.toField x, euclideanMemL2 := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldNeg_apply {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) (x : Vec d) : (centeredCubeEuclideanL2FieldNeg F).toField x = -F.toField x

noncomputable def HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldSub {d : ℕ} {m : ℤ} (F G : CenteredCubeEuclideanL2Field d m) : CenteredCubeEuclideanL2Field d m

Pointwise subtraction, packaged through addition and negation on the centered-cube Euclidean L2 carrier.

Equations

• HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldSub F G = HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldAdd F (HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldNeg G)

@[simp]

theorem HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldSub_apply {d : ℕ} {m : ℤ} (F G : CenteredCubeEuclideanL2Field d m) (x : Vec d) : (centeredCubeEuclideanL2FieldSub F G).toField x = F.toField x - G.toField x