High-contrast homogenization: Provider.Regularity.UnitCubeDirichletContinuousKIntegralSplit

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

Split continuous K-energy for the unit-cube Dirichlet map

The low-scale rescaling estimate is paired with the complementary root-scale interval. On that interval the zero competitor and the exact normalized Euclidean L² energy inequality give a closed-form endpoint contribution.

theorem HCPolySupport.HighContrast.exists_unitCubeDirichletContinuousKIntegralSplitBound (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 ∧ ∫⁻ (t : ℝ) in Set.Ioo A⁻¹ 1, continuousKSeminormIntegrand (↑s) (unitCubeGradientEuclideanL2Field w) t ≤ ENNReal.ofReal ((A.rpow (2 * ↑s) - 1) / (2 * ↑s)) * (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 h.toField ^ 2

One dimension-dependent expansion factor, fixed before all analytic inputs, simultaneously gives the exact low-scale rescaling bound and the closed-form normalized-L² bound on the complementary root interval.