High-contrast homogenization: Provider.PolynomialHomogenization.ScheduledLocalizationRowSupply

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

The scheduled localization hypothesis from a ruled Whitney row supply

The scheduled localization clause consumes the scheduled localization hypothesis: on the gauge-reduced domain it asks for a ruled scheduled localization package together with the two normalized Whitney row-energy caps of the corrector difference and of the flux defect.

This module discharges every part of that demand which does not require a new estimate — the gauge-reduced geometry, the elliptic source representative, the Hardy coefficient, the distortion factor, the boundary energy, and the whole package assembly — and isolates what remains as a single named supply, ScheduledLocalizationRowSupply, stated at exactly the scheduled spelling.

The residual supply

Package assembly with the two rows retained

theorem HCPolySupport.HighContrast.memVectorL2_physical_flux_difference {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (aSource : Source.AKL.Field d) (haSource : AEUniformlyEllipticField aSource) (aPhysical : CoeffField d) (haeSource : ↑aSource =ᵐ[MeasureTheory.volume] aPhysical) (u h : H1Function U) : MemVectorL2 U fun (y : Vec d) => matVecMul (aPhysical y) (u.grad y) - h.grad y

The physical flux difference of an a.e. uniformly elliptic coefficient is square integrable on a bounded convex domain.