High-contrast homogenization:

Provider.Regularity.CenteredCubeDirichletNormalizedEuclideanL2Residual

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

Normalized Euclidean L2 residual stability for the identity Dirichlet problem

The physical normalized Euclidean L² endpoint is stable under subtraction: the difference of two identity Dirichlet solution gradients is controlled by the difference of their data with constant one.

theorem HCPolySupport.HighContrast.centeredCubeDirichletDivergence_normalizedEuclideanLpENorm_grad_sub_le {d : ℕ} {m : ℤ} (h k : CenteredCubeEuclideanL2Field d m) (w v : H10Function (openCubeSet (originCube d m))) (hw : CubeDirichletDivergenceProblem (originCube d m) w h.toField) (hv : CubeDirichletDivergenceProblem (originCube d m) v k.toField) : ((centeredCubeDomain d m).normalizedEuclideanLpENorm 2 fun (x : Vec d) => w.grad x - v.grad x) ≤ (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 fun (x : Vec d) => h.toField x - k.toField x

Two identity Dirichlet solutions are nonexpansive on differences in the physical normalized Euclidean L² norm.