Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedUnitCubeContinuousKNormalizedEnergyIdentityDefect

High-contrast homogenization: #

Provider.Regularity.RoundedUnitCubeContinuousKNormalizedEnergyIdentityDefect

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

Rounded identity defect on the normalized unit-cube continuous K-energy #

The rounded reference differs from the identity by at most 1/100 in the Euclidean matrix operator norm. The constant-matrix action on the quadratic continuous K-energy therefore yields the exact squared defect factor.

source
theorem HCPolySupport.HighContrast.unitCubeNormalizedContinuousKEnergy_roundedReferenceMatrix_sub_one_mul_le {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
(unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 (unitCubeEuclideanL2FieldConstMatrixMul (roundedReferenceMatrix abar hS - 1) F).toField ^ 2 + ENNReal.ofReal (2 * ↑s) * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) (unitCubeEuclideanL2FieldConstMatrixMul (roundedReferenceMatrix abar hS - 1) F) t ≤ ENNReal.ofReal ((1 / 100) ^ 2) * ((unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField ^ 2 + ENNReal.ofReal (2 * ↑s) * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) F t)

The rounded reference identity defect contracts the normalized quadratic continuous K-energy by the square of the fixed one-percent factor.