High-contrast homogenization: Provider.Regularity.CenteredCubeEuclideanHsAddition

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

Addition on the physical centered-cube Euclidean Hs carrier

This module packages pointwise addition on the proof-carrying physical Euclidean L2 carrier. The elementary squared triangle estimate gives a dimension-free bound for the literal centered-cube Gagliardo energy, and hence addition preserves MemCenteredCubeEuclideanHs.

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

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

Equations

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

@[simp]

theorem HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldAdd_apply {d : ℕ} {m : ℤ} (F G : CenteredCubeEuclideanL2Field d m) (x : Vec d) : (centeredCubeEuclideanL2FieldAdd F G).toField x = F.toField x + G.toField x