High-contrast homogenization:

Provider.Regularity.RoundedCenteredCubeDirichletEuclideanHsRegularity

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

Rounded-reference Euclidean fractional regularity on centered cubes

The rounded-reference unit-cube response is pushed forward by the normalized centered-cube dilation. Its gradient is unchanged under pullback, the constant-coefficient weak equation is preserved exactly, and the homogeneous physical Euclidean fractional full norm gives the same scale factor on the input and output. Thus the unit-cube constant controls every centered triadic scale.

theorem HCPolySupport.HighContrast.unitCenteredOpenCube_eq_inv_smul_centeredOpenCube_rounded {d : ℕ} (m : ℤ) : openCubeSet (originCube d 0) = (centeredCubeScale m)⁻¹ • openCubeSet (originCube d m)

noncomputable def HCPolySupport.HighContrast.roundedCenteredCubeNormalizedPushforward {d : ℕ} (m : ℤ) (u : H10Function (openCubeSet (originCube d 0))) : H10Function (openCubeSet (originCube d m))

Inverse normalized dilation of a unit-cube zero-trace response to the physical centered cube.

Equations

• HCPolySupport.HighContrast.roundedCenteredCubeNormalizedPushforward m u = HCPolySupport.centeredCubeScale m • HCPolySupport.H10Function.unscale ⋯ (⋯ ▸ u)

theorem HCPolySupport.HighContrast.exists_roundedCenteredCubeDirichletEuclideanHsRegularity (d : ℕ) [NeZero d] : ∃ (s : ↑FractionalOrder), ↑s < 1 / 12 ∧ ∃ C < ⊤, ∀ (m : ℤ) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : CenteredCubeEuclideanL2Field d m), MemCenteredCubeEuclideanHs s h → ∃ (w : H10Function (openCubeSet (originCube d m))), (IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedReferenceMatrix abar hS)) (openCubeSet (originCube d m)) w fun (y : Vec d) => -h.toField y) ∧ MemCenteredCubeEuclideanHs s (centeredCubeGradientEuclideanL2Field w) ∧ centeredCubeEuclideanHsFullENorm s (centeredCubeGradientEuclideanL2Field w) ≤ C * centeredCubeEuclideanHsFullENorm s h

One selected order and one finite constant control rounded-reference zero-trace responses on every centered triadic cube. Physical output membership and the homogeneous full-norm estimate are conclusions.