High-contrast homogenization:

Provider.PolynomialHomogenization.Root.EnergyPrice.ResidualWindowFillingBound

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

The filling coefficient on the residual window λ ∈ [1,3]

The energy leg never evaluates observationFillingCoefficient at the physical ε: RowRetainingPrintOrderGoodScale.exists_residualFrameResponseRate evaluates it at the residual dilation λ = ε·3^N ∈ Set.Icc 1 3 produced by the triadic ε-frame transport RowRetainingPrintOrderGoodScale.exists_scaledResponseWindowTail, whose hypotheses are exactly the binder surface used here.

HCPoly.Provider.PolynomialHomogenization.Root.EnergyPrice.FillingCoefficientAbsorption bounded the coefficient for ε ≤ 1. The residual window needs λ ≤ 3, so the absorption is restated here with an arbitrary upper bound on the dilation.

theorem HCPolySupport.HighContrast.EnergyPrice.observationFillingCoefficient_le_of_boundedDilation {d : ℕ} [NeZero d] {abar : Mat d} {U : Set (Vec d)} {cc : Vec d} {epsilon B Rad : ℝ} (hS : Matrix.PosDef (symmPart abar)) (hepsilon : 0 < epsilon) (hepsilonB : epsilon ≤ B) (hRad : 0 ≤ Rad) (hInner : ellipsoid abar (1 / (3 * √↑d)) ⊆ U) (hOut : matImage (matSqrt (symmPart abar))⁻¹ U ⊆ euclideanBallAt cc Rad) : RowSupply.observationFillingCoefficient d epsilon abar ≤ max 1 (18 * ↑d ^ 2 * B * Rad)

The filling coefficient under a bounded dilation. The absolute gauge scale α is absorbed by the inner-ellipsoid premise and the consumer's outer ball; the dilation contributes only its own upper bound.

theorem HCPolySupport.HighContrast.EnergyPrice.observationFillingCoefficient_le_of_residualWindow {d : ℕ} [NeZero d] {abar : Mat d} {U : Set (Vec d)} {cc : Vec d} {lambda Rad : ℝ} (hS : Matrix.PosDef (symmPart abar)) (hlambda : lambda ∈ Set.Icc 1 3) (hRad : 0 ≤ Rad) (hInner : ellipsoid abar (1 / (3 * √↑d)) ⊆ U) (hOut : matImage (matSqrt (symmPart abar))⁻¹ U ⊆ euclideanBallAt cc Rad) : RowSupply.observationFillingCoefficient d lambda abar ≤ max 1 (54 * ↑d ^ 2 * Rad)

The residual-window instance. On the residual window λ ∈ [1,3] the filling coefficient is bounded by a function of d and the outer radius only — the form the energy leg needs.