High-contrast homogenization: Provider.Quenched.SmallContrastBadLevelResidue

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

At the matched threshold the good-set residue is zero, and the source leg stays geometric

The two machine questions the released level has to answer before it is worth releasing anywhere.

Does the residue vanish? The residue enters because the excess is taken above a threshold below the maximum's own deterministic level: with the level held at 1 / 2 and the almost-sure envelope at R / 2, the excess off the bad event is bounded by (R - 1) / 2 rather than by 0, and its fourth power is the constant summand of the scaled bad-moment majorant. The vanishing of the good-set excess below is the one line that changes when the threshold is matched to the envelope, and lintegral_pow_eq_setLIntegral_of_matched_threshold is its consequence for the moment: the good set contributes nothing at all, so the moment bound is the bad-set bound with no additive term.

Does the source leg stay geometric? This is the residue's own fail-closed requirement: nonnegativity of a replacement majorant is not enough, it must admit the geometric leg in the shape the entry-slot clause reads. profileBadMajorantAt_badMoment_le is that leg at the released level, and the start bound is it at the account's own use site — the same shape as the established pair, with one Π-polynomial factor R in front of a constant the source slot already permits to be Π-polynomial.

Nothing here is imported by any established file.

The residue vanishes at the matched threshold

theorem HCPolySupport.HighContrast.Quenched.lintegral_pow_eq_setLIntegral_of_matched_threshold {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {Q beta : ℝ} (hQ : 0 < Q) {M W : Ω → ENNReal} {G : Set Ω} (hG : MeasurableSet G) (hWdef : ∀ (a : Ω), W a = M a - ENNReal.ofReal beta) (hgood : ∀ᵐ (a : Ω) ∂P, a ∉ G → M a ≤ ENNReal.ofReal beta) : ∫⁻ (a : Ω), W a ^ Q ∂P = ∫⁻ (a : Ω) in G, W a ^ Q ∂P

The moment loses its constant summand. When the threshold is matched to the good-set envelope, the excess vanishes off the bad set and the moment integral is the bad set's alone — no residue is added.

The source leg is still geometric

theorem HCPolySupport.HighContrast.Quenched.profileBadMajorantAt_badMoment_le (K : ℝ) {R : ℝ} (hR : 1 ≤ R) {Delta : ℤ} (hD : 0 ≤ Delta) : Response.profileBadMajorantAt 4 (R ^ 4 * badMomentMajorant K Delta) (R / 2) R ≤ R * badSourceConstant K * 3 ^ (-(1 / 2) * ↑Delta)

The geometric bad-event leg at the released level. The counterpart of the profile bad-majorant moment bound, for the residue-free majorant R ^ 4 · badMomentMajorant at the matched threshold (beta, lev) = (R / 2, R). The rate is the printed half rate, unchanged; the cost of the released level is the single factor R.