High-contrast homogenization: Provider.Quenched.SmallContrastEntryRateAtLevel

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

The bad-event leg at the matched threshold

The source group's bad leg with the residue-free majorant in place of the pinned one. The rate is unchanged — the printed half rate in the absolute-generation gap — and the only cost of the matched threshold is the single factor R in front of a constant the source slot already permits to carry the grid's aspect ratio.

noncomputable def HCPolySupport.HighContrast.Quenched.badSourceLegConstantAtLevel (L K R : ℝ) : ℝ

The bad-event leg's assembled constant at the matched threshold.

Equations

• HCPolySupport.HighContrast.Quenched.badSourceLegConstantAtLevel L K R = √2 * √(L + 1) * (R * HCPolySupport.HighContrast.Quenched.badSourceConstant K) + √2 * √(L + 1)

theorem HCPolySupport.HighContrast.Quenched.bad_source_leg_at_level_le {L K R : ℝ} (hR : 1 ≤ R) {Delta : ℤ} (hD : 0 ≤ Delta) {g : ℝ} {Hw : ℕ} {beta : ℝ} {N : ℕ} (hDrate : beta * ↑N ≤ 1 / 2 * ↑Delta) (hHrate : beta * ↑N ≤ contrastAlpha g * ↑Hw) : √2 * √(L + 1) * Response.profileBadMajorantAt 4 (R ^ 4 * badMomentMajorant K Delta) (R / 2) R + √2 * 3 ^ (-((1 - contrastRho g) / 2) * ↑Hw) * √(L + 1) ≤ badSourceLegConstantAtLevel L K R * 3 ^ (-beta * ↑N)

The bad-event leg at the common rate, at the matched threshold.