High-contrast homogenization: Provider.Quenched.SmallContrastRawPrefactorCap #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.Quenched.corrected_cadence_raw_prefactor_cap
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{lAl : ℤ}
{E : BlockMat d}
{N₀ ns cA : ℕ}
{A alpha b0 bA b2 S0 S1 S2 d0 base Cns C7 cns ct2 : ℝ}
(hbase : 3 ≤ base)
(hfloor0 : 0 ≤ hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ 0)
(hfloor : hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ 0 ≤ 1 / 9)
(hrate0 : 0 ≤ linRate A alpha b0 bA b2 cA S0)
(hrate4 : linRate A alpha b0 bA b2 cA S0 ≤ 1 / 4)
(hCns : 1 ≤ Cns)
(hC7 : 1 ≤ C7)
(hcns : 0 ≤ cns)
(hct2 : 0 ≤ ct2)
(hstart : 3 ^ ↑(linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0) ≤ Cns ^ 2 * C7 * base.rpow (2 * cns + ct2))
:
The raw corrected-cadence prefactor follows from the polynomial cap on the initial level-schedule index, the floor bound, and the quarter-rate bound.