Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.UnitCubeDirichletContinuousKSmallOrder

High-contrast homogenization: Provider.Regularity.UnitCubeDirichletContinuousKSmallOrder #

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

Small-order normalized continuous K-energy #

The expansion factor in the normalized quadratic estimate is fixed by the dimension. Continuity of real powers at order zero then selects one positive fractional order, before the datum and solution, for which the exact loss is strictly below 101/100.

source
theorem HCPolySupport.HighContrast.exists_unitCubeDirichletContinuousKNormalizedEnergySmallOrder (d : ℕ) [NeZero d] :
∃ (A : ℝ), 1 ≤ A ∧ ∃ (s : ↑FractionalOrder), ↑s < 1 / 12 ∧ ENNReal.ofReal A ^ (2 * ↑s) < ENNReal.ofReal (101 / 100) ∧ ∀ (h : UnitCubeEuclideanL2Field d) (w : H10Function (openCubeSet (originCube d 0))), CubeDirichletDivergenceProblem (originCube d 0) w h.toField → (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 (unitCubeGradientEuclideanL2Field w).toField ^ 2 + ENNReal.ofReal (2 * ↑s) * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) (unitCubeGradientEuclideanL2Field w) t ≤ ENNReal.ofReal A ^ (2 * ↑s) * ((unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 h.toField ^ 2 + ENNReal.ofReal (2 * ↑s) * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) h t)

For each positive dimension, one expansion factor and one fractional order below 1/12 can be fixed before the analytic inputs so that the exact normalized continuous K-energy loss is strictly below 101/100.