High-contrast homogenization: Provider.Quenched.SmallContrastCorrectedConstantBounds

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

Lower bounds for the corrected cadence constants

These elementary bounds expose the normalization facts used by the corrected cadence level schedule. Their statements are written at the defining expressions of the four constants, so the endpoint only rewrites its local set equations.

theorem HCPolySupport.HighContrast.Quenched.one_le_corrected_generation_coefficient {H : ℕ} {C5 CF rate : ℝ} (hC5 : 1 ≤ C5) (hCF : 1 ≤ CF) (hrate : 0 < rate) : 1 ≤ 3 ^ (H + 1) * 624 * (8100 * 3 ^ (3 * H) * C5 ^ 4) * (3 * CF.rpow rate⁻¹) * 3

The coefficient multiplying the generation cap is at least one.

theorem HCPolySupport.HighContrast.Quenched.one_le_corrected_bad_source_coefficient {d : ℕ} {Cpre X : ℝ} (hCpre : 1 ≤ Cpre) : 1 ≤ 1 + 6 * weakCoefficient d Cpre * X ^ 2 * 65536

The bad-source coefficient is one plus a nonnegative square term.

theorem HCPolySupport.HighContrast.Quenched.one_le_corrected_source_coefficient {d : ℕ} {Cpre X t : ℝ} (hCpre : 1 ≤ Cpre) : 1 ≤ 1 + 6 * weakCoefficient d Cpre * X ^ 2 * Real.rpow 3 t

The fixed source coefficient is one plus a nonnegative source payment.

theorem HCPolySupport.HighContrast.Quenched.one_le_corrected_ledger_coefficient {delta CX beta : ℝ} (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (hCX : 1 ≤ CX) (hbeta : 0 < beta) : 1 ≤ 3 / delta ^ 2 * 3 * (CX / delta ^ 2).rpow beta⁻¹

The coefficient paying the two source ceilings is at least one.