High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.RateFactorToHoleShape

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

The rate factor, from the capstone's shape to the hole's

that module concludes at the capstone's own length x · eccentricityFoldFactor abar p₀ and at whatever constant the caller supplies. The clause reads its rate factor at x · (Lg · eccentricityFoldFactor abar pEcc) with a law-free constant.

the constant_and_eccentricity_absorbed premise performs the two absorptions; this module wraps it for the ℝ≥0∞-valued conclusion, so that a real-valued class split of the capstone's constant (module that module) is all the caller has to supply.

theorem HCPolySupport.HighContrast.RowSupply.rateFactor_to_holeShape {d : ℕ} (abar : Mat d) {Hconst Claw Krest p p0 kappa epsilon x : ℝ} {A B : ENNReal} (hbound : A ≤ ENNReal.ofReal (Hconst * (epsilon * (x * eccentricityFoldFactor abar p0)) ^ kappa) * B) (hHle : Hconst ≤ Claw * max 1 (witnessEccentricity (symmPart abar)) ^ p * Krest) (hClaw : 0 ≤ Claw) (hkappa : 0 < kappa) (hp : 0 ≤ p) (hp0 : 0 ≤ p0) (heps : 0 ≤ epsilon) (hx : 0 ≤ x) : A ≤ ENNReal.ofReal (Claw * (epsilon * (x * (perGLengthFactor Krest kappa * eccentricityFoldFactor abar (p0 + p / kappa)))) ^ kappa) * B

The hole's rate factor from the capstone's. A bound at the capstone's length and constant, together with a class split of that constant, gives the bound at the hole's length and at the law-free head.