High-contrast homogenization:

Provider.PolynomialHomogenization.Root.EnergyPrice.ForceBesovFromHsNormSq

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

Gate R2-besov: ForceBesovRegularity from the Euclidean fractional carrier

The frozen clause supplies the datum's regularity as hsNormSq U s₀ g₀.grad ≠ ⊤ while the upstream Dirichlet energy package asks for ForceBesovRegularity. No producer of the latter from the former exists anywhere in this development.

HCPoly.Provider.PolynomialHomogenization.Root.BufferToCell.PositiveBesovContinuousComparison has a private bridge forceSobolevRegularity_of_hsNormSq_lt_top whose ForceBesovRegularity premise is consumed only through .memLp, at two sites, and whose MemVectorL2 premise is consumed only through .1. That declaration is private, so the bridge and its one private measurability helper are re-proved below with the premise weakened to bare MemLp — the "one-hypothesis swap". Composing with upstream ForceSobolevRegularity.toForceBesovRegularity closes the gate.

theorem HCPolySupport.HighContrast.EnergyPrice.scalarGagliardoKernel_aestronglyMeasurable' {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (hFnorm : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure Q)) (hFcube : MeasureTheory.AEStronglyMeasurable F (cubeMeasure Q)) (i : Fin d) : MeasureTheory.AEStronglyMeasurable (Gagliardo.gagliardoKernel s 2 fun (x : Vec d) => F x i) (Gagliardo.gagliardoCubeMeasure Q)

Re-proof of a private Gagliardo-kernel measurability helper.

theorem HCPolySupport.HighContrast.EnergyPrice.forceSobolevRegularity_of_hsNormSq_lt_top' {d : ℕ} [NeZero d] (Q : TriadicCube d) (sF : ↑FractionalOrder) (F : Vec d → Vec d) (hmem : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hFcube : MemVectorL2 (openCubeSet Q) F) (hHs : hsNormSq (openCubeSet Q) (↑sF) F < ⊤) : Book.Ch03.Legacy.ForceSobolevRegularity Q (↑sF) F

The swapped bridge. The ForceBesovRegularity premise of the private bridge is replaced by bare MemLp; the proof is otherwise unchanged.

theorem HCPolySupport.HighContrast.EnergyPrice.forceBesovRegularity_of_hsNormSq_ne_top {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hs1 : s < 1) (F : Vec d → Vec d) (hmem : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hFcube : MemVectorL2 (openCubeSet Q) F) (hHs : hsNormSq (openCubeSet Q) s F ≠ ⊤) : Book.Ch03.ForceBesovRegularity Q s F

Gate R2-besov, closed. The Chapter 3 Besov regularity of a field follows from its MemLp membership, its square integrability on the cube, and the finiteness of HCPoly's Euclidean fractional carrier at the same order.