High-contrast homogenization: Provider.Quenched.Prop211Cost

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

Polynomial cost of the one-time rebase

theorem HCPolySupport.HighContrast.Quenched.fixed_le_rpow_of_three_le {C base : ℝ} (hC : 1 ≤ C) (hbase : 3 ≤ base) : C ≤ base ^ Real.logb 3 C

A fixed positive factor is absorbed by a power of any base at least three.

theorem HCPolySupport.HighContrast.Quenched.rebase_generation_cost {base Centry : ℝ} {mEnt q A D : ℕ} (hbase : 3 ≤ base) (hentry : 3 ^ mEnt ≤ 3 * base ^ Centry) (hq : 3 ^ ↑q ≤ base ^ 4) : 3 ^ (mEnt + (A + D + 1) * q) ≤ base ^ (1 + Centry + 4 * ↑(A + D + 1))

The generation selected from an entry scale and a bracket index has a law-independent polynomial cost.

theorem HCPolySupport.HighContrast.Quenched.renormalizedCombinedGrowthWitness_le_rpow (d : ℕ) {mu base K : ℝ} {B q : ℕ} (hmu : 0 < mu) (hbase : 3 ≤ base) (hK : K ≤ base) (hq : 3 ^ ↑q ≤ base ^ 4) : renormalizedCombinedGrowthWitness d (B * q) mu K ≤ base ^ (2 * (1 + 4 * ↑B + Real.logb 3 (frPoweredGrowthWitness d mu)))

The combined growth witness has polynomial size in the original polynomial base.

theorem HCPolySupport.HighContrast.Quenched.rebase_reference_cost {base aspect aspectNew Knew Casp eK : ℝ} (hbase : 3 ≤ base) (haspectOne : 1 ≤ aspect) (haspect : aspect ≤ base) (hCasp : 1 ≤ Casp) (haspectNew : 1 ≤ aspectNew) (hKnew : 1 ≤ Knew) (haspectBound : aspectNew ≤ Casp * aspect) (hKcost : Knew ≤ base ^ eK) : 2 + aspectNew * Knew ≤ base ^ (2 + Real.logb 3 Casp + eK)

A fixed aspect-ratio loss and a polynomial growth witness combine into one polynomial reference cost.