High-contrast homogenization: Provider.Regularity.CenteredCubeDirichletNormalizedEuclideanL2Energy

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

Normalized Euclidean L2 energy for the identity Dirichlet problem

The sharp identity-coefficient energy endpoint is expressed here in the normalized Euclidean L² norm on every physical centered cube. The constant remains exactly one, with no dimension or cube-volume loss.

noncomputable def HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldAsCubeTwo {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : CubeEuclideanL2LpField (originCube d m) FiniteLpExponent.two

View a centered-cube Euclidean L² field as an exponent-two CubeEuclideanL2LpField on originCube d m.

Equations

• HCPolySupport.HighContrast.centeredCubeEuclideanL2FieldAsCubeTwo F = { toField := F.toField, euclideanMemLp := ⋯, euclideanMemL2 := ⋯ }

theorem HCPolySupport.HighContrast.centeredCubeDirichletDivergence_normalizedEuclideanLpENorm_grad_le {d : ℕ} {m : ℤ} (h : CenteredCubeEuclideanL2Field d m) (w : H10Function (openCubeSet (originCube d m))) (hproblem : CubeDirichletDivergenceProblem (originCube d m) w h.toField) : (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 (centeredCubeGradientEuclideanL2Field w).toField ≤ (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 h.toField

The identity Dirichlet solution map is nonexpansive in the physical normalized Euclidean L² norm.