High-contrast homogenization: Provider.Regularity.UnitCubeDirichletContinuousKNormalizedEnergy

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

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

The low and root scale intervals are recombined after multiplying the continuum energy by 2s. The exact endpoint contribution then merges with the normalized Euclidean L² square, leaving the sharp factor A^(2s).

theorem HCPolySupport.HighContrast.exists_unitCubeDirichletContinuousKNormalizedEnergyBound (d : ℕ) [NeZero d] : ∃ (A : ℝ), 1 ≤ A ∧ ∀ (s : ↑FractionalOrder) (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)

A dimension-dependent expansion factor, fixed before the fractional order and analytic inputs, controls the normalized quadratic continuous K-energy of the unit-cube identity Dirichlet gradient by the datum energy with the exact multiplier A^(2s).