High-contrast homogenization: Provider.Quenched.SmallContrastSplitRateCheck

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

The corrected rate at the split supply

The level schedule's conclusion rate linRate is antitone in the recursion constant and in the lag-channel coefficient, and the burn-split supply value is capped by a pre-law constant once κ_𝐄 ≤ 1 + 6σ. Together these certify that fixing the rate at the pre-law caps only weakens the conclusion. Dependence on Π and the aspect ratio occurs only in scale thresholds, not in the rate.

theorem HCPolySupport.HighContrast.Quenched.linCs_mono {A A' alpha b0 bA b2 : ℝ} {cA : ℕ} {S0 S0' : ℝ} (hA : 1 ≤ A) (hAA' : A ≤ A') (hb0 : 0 < b0) (hS0 : 1 ≤ S0) (hSS' : S0 ≤ S0') : linCs A alpha b0 bA b2 cA S0 ≤ linCs A' alpha b0 bA b2 cA S0'

The spacing constant is monotone in the recursion constant and the lag coefficient.

theorem HCPolySupport.HighContrast.Quenched.linRate_anti {A A' alpha b0 bA b2 : ℝ} {cA : ℕ} {S0 S0' : ℝ} (hA : 1 ≤ A) (hAA' : A ≤ A') (halpha : 0 < alpha) (hb0 : 0 < b0) (hbA : 0 < bA) (hb2 : 0 < b2) (hS0 : 1 ≤ S0) (hSS' : S0 ≤ S0') : linRate A' alpha b0 bA b2 cA S0' ≤ linRate A alpha b0 bA b2 cA S0

The conclusion rate is antitone in the recursion constant and the lag coefficient.

theorem HCPolySupport.HighContrast.Quenched.linRate_pos {A alpha b0 bA b2 : ℝ} {cA : ℕ} {S0 : ℝ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hb0 : 0 < b0) (hbA : 0 < bA) (hb2 : 0 < b2) (hS0 : 1 ≤ S0) : 0 < linRate A alpha b0 bA b2 cA S0

The conclusion rate is positive.

theorem HCPolySupport.HighContrast.Quenched.supplyMscSplit_le {d : ℕ} {E : BlockMat d} {kapBar : ℝ} (hkap : kappaRef E ≤ kapBar) : supplyMscSplit d E ≤ (2 * ↑d) ^ 2⁻¹ * (kapBar * 4) * (2 * 4) * √2

The split supply value is capped by the pre-law reference bound.

theorem HCPolySupport.HighContrast.Quenched.vsumSourceConstant_mono {d : ℕ} {Csub delta : ℝ} (hCsub : 0 ≤ Csub) {Msc Msc' : ℝ} (hMM' : Msc ≤ Msc') : vsumSourceConstant d Csub Msc delta ≤ vsumSourceConstant d Csub Msc' delta

The variance-leg constant is monotone in the supply value.