High-contrast homogenization: Provider.Regularity.UnitCubeDirichletContinuousKLowScaleIntegral

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

Low-scale continuous K-energy for the unit-cube Dirichlet map

The exact rescaled pointwise comparison is integrated on the interval where the expanded parameter remains in the source carrier. The Jacobian and the interpolation weight combine to give precisely the factor A^(2s).

theorem HCPolySupport.HighContrast.exists_unitCubeDirichletContinuousKLowScaleIntegralBound (d : ℕ) [NeZero d] : ∃ (A : ℝ), 1 ≤ A ∧ ∀ (s : ↑FractionalOrder) (h : UnitCubeEuclideanL2Field d) (w : H10Function (openCubeSet (originCube d 0))), CubeDirichletDivergenceProblem (originCube d 0) w h.toField → ∫⁻ (t : ℝ) in Set.Ioo 0 A⁻¹, continuousKSeminormIntegrand (↑s) (unitCubeGradientEuclideanL2Field w) t ≤ ENNReal.ofReal A ^ (2 * ↑s) * ∫⁻ (u : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) h u

A dimension-dependent expansion factor can be selected before the fractional order, datum, and solution so that the low-scale continuous K-energy is bounded with the exact factor A^(2s).