High-contrast homogenization:

Provider.Regularity.RoundedUnitCubeDirichletContinuousKDefectResponseContraction

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

Small-order contraction of the rounded defect response

The identity Dirichlet response is evaluated at the rounded reference identity-defect datum. The selected small-order expansion factor and the one-percent matrix-defect action combine to give a strict quadratic-energy contraction, with every coefficient inequality derived before the later matrix, field, and solution binders.

theorem HCPolySupport.HighContrast.exists_roundedUnitCubeDirichletContinuousKDefectResponseContraction (d : ℕ) [NeZero d] : ∃ (A : ℝ), 1 ≤ A ∧ ∃ (s : ↑FractionalOrder), ↑s < 1 / 12 ∧ ENNReal.ofReal A ^ (2 * ↑s) < ENNReal.ofReal (101 / 100) ∧ ENNReal.ofReal A ^ (2 * ↑s) * ENNReal.ofReal ((1 / 100) ^ 2) < ENNReal.ofReal (101 / 1000000) ∧ ENNReal.ofReal A ^ (2 * ↑s) * ENNReal.ofReal ((1 / 100) ^ 2) < 1 ∧ ∀ (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (F : UnitCubeEuclideanL2Field d) (w : H10Function (openCubeSet (originCube d 0))), CubeDirichletDivergenceProblem (originCube d 0) w (unitCubeEuclideanL2FieldConstMatrixMul (roundedReferenceMatrix abar hS - 1) F).toField → unitCubeNormalizedContinuousKEnergy s (unitCubeGradientEuclideanL2Field w) ≤ ENNReal.ofReal A ^ (2 * ↑s) * ENNReal.ofReal ((1 / 100) ^ 2) * unitCubeNormalizedContinuousKEnergy s F

For each positive dimension, the small fractional order selected for the identity Dirichlet response also makes the response to the rounded identity defect a strict contraction in the normalized quadratic continuous K-energy.