High-contrast homogenization: Provider.Regularity.CenteredCubeEuclideanHsConstantMatrix

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

Constant matrices on the physical centered-cube Euclidean Hs carrier

The rounded reference is controlled in the Euclidean matrix operator norm. This module keeps that norm all the way through the physical fractional carrier: constant matrix multiplication preserves the stored Euclidean L2 field, multiplies its squared Gagliardo energy by at most the square of the matrix norm, and therefore preserves MemCenteredCubeEuclideanHs.

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

Pointwise constant-matrix multiplication, packaged as a centered-cube Euclidean L2 field.

Equations

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

@[simp]

theorem HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldConstMatrixMul_apply {d : ℕ} {m : ℤ} (A : Mat d) (F : CenteredCubeEuclideanL2Field d m) (x : Vec d) : (centeredCubeEuclideanL2FieldConstMatrixMul A F).toField x = matVecMul A (F.toField x)