High-contrast homogenization: Provider.Regularity.CenteredCubeEuclideanHsFullNormConstantMatrix

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

Constant matrices on the physical centered-cube Euclidean Hs full norm

The physical homogeneous full norm combines a scale-weighted normalized Euclidean L2 term with the square root of the Gagliardo energy. Constant matrix multiplication acts on both terms with the Euclidean matrix operator norm, so the resulting estimate is dimension-free.

theorem HCPolySupport.HighContrast.euclideanNorm_matVecMul_le_l2_opNorm {d : ℕ} (A : Mat d) (x : Vec d) : euclideanNorm (matVecMul A x) ≤ ‖A‖ * euclideanNorm x

The Euclidean operator norm controls pointwise constant-matrix multiplication in the explicit Euclidean vector magnitude.

theorem HCPolySupport.HighContrast.centeredCubeNormalizedEuclideanLpENorm_constMatrixMul_le {d : ℕ} {m : ℤ} (A : Mat d) (F : CenteredCubeEuclideanL2Field d m) : (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 (centeredCubeEuclideanL2FieldConstMatrixMul A F).toField ≤ ENNReal.ofReal ‖A‖ * (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 F.toField

Constant matrix multiplication scales the normalized physical Euclidean L2 term by at most the Euclidean matrix operator norm.