Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedPhysicalDirichletEuclideanHs

High-contrast homogenization: Provider.Regularity.RoundedPhysicalDirichletEuclideanHs #

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

Uniform rounded physical Dirichlet Euclidean Hs provider #

The all-scale rounded-reference regularity theorem is composed with the quotient-first affine response. One fractional order and one finite constant are selected before every scale, effective matrix, and datum. The normalized full-norm estimate and the physical weak, quotient, and affine-loss conclusions are exported together.

source
theorem HCPolySupport.HighContrast.exists_roundedPhysicalDirichletEuclideanHsConstant (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 ∧ ∃ (wPhysical : H10Function (roundedPhysicalCube abar m)), (wPhysical.toFun = fun (x : Vec d) => w.toFun (matVecMul (baseRoundedGrid (symmPart abar))⁻¹ x)) ∧ (wPhysical.grad = fun (x : Vec d) => matVecMul (baseRoundedGrid (symmPart abar))⁻¹ (w.grad (matVecMul (baseRoundedGrid (symmPart abar))⁻¹ x))) ∧ (IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedPhysicalReferenceMatrix abar)) (roundedPhysicalCube abar m) wPhysical fun (x : Vec d) => -roundedPhysicalDirichletDatum abar h x) ∧ wPhysical.gradToHilbertVectorL2 = affineGradientQuotientPushforward ⋯ ⋯ ⋯ (baseRoundedGrid (symmPart abar))⁻¹ w.gradToHilbertVectorL2 ∧ hsNormSq (roundedPhysicalCube abar m) (↑s) wPhysical.grad ≤ roundedPhysicalGradientHsLoss abar ↑s * hsNormSq (openCubeSet (originCube d m)) (↑s) w.grad

One selected order and finite constant simultaneously supply the rounded-reference centered-cube response and its quotient-first physical affine representative.