High-contrast homogenization: Provider.Regularity.CenteredCubeEuclideanHsFullNormAddition

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

Addition on the physical centered-cube Euclidean Hs full norm

Pointwise addition obeys Minkowski's inequality on the normalized Euclidean L2 term. Combining that estimate with the squared-energy triangle bound gives a dimension-free addition estimate for the homogeneous physical fractional full norm.

theorem HCPolySupport.HighContrast.centeredCubeNormalizedEuclideanLpENorm_add_le {d : ℕ} {m : ℤ} (F G : CenteredCubeEuclideanL2Field d m) : (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 (centeredCubeEuclideanL2FieldAdd F G).toField ≤ (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 F.toField + (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 G.toField

Minkowski's inequality for pointwise addition on the normalized physical Euclidean L2 term.