High-contrast homogenization: Provider.Quenched.SmallContrastSmallnessPack

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

The per-generation smallness pack and the drop slot

Two of the four analytic families of hypotheses of exists_account_one_step_entry_of_block_at_level come from the bootstrap's single scalar smallness d(Θ̂_r − 1) ≤ δ alone. This file discharges them.

• The contrast smallness 6(Θ(E_t) − 1) ≤ 1. The hatted-to-intrinsic comparison (the hatted-polynomial contrast bound) gives Θ − 1 ≤ (5/4)F + (1/4)F² at F = d(Θ̂ − 1), so δ ≤ 1/9 suffices: 6((5/4)(1/9) + (1/4)(1/81)) = 46/54 < 1.
• The drop smallness d(Θ̂_j − Θ̂_p) ≤ 1 at every depth: the hatted contrast is ≥ 1, so every drop is below the excess at its upper scale.

It also records the drop slot in recursion shape: meanDrop2ValueIsotropy — the carrier exists_account_one_step_entry_of_block_at_level consumes in its Dr slot — is literally 4·(F_{t-j} - F_t)·c_T, i.e. the c_D·(F(n-j) - F n) shape of hrec_final_sharp_at_jb_src, with c_D = 4 c_T and

c_T = 2·boundaryConst Cd g mAl·3^{g G}·blockSize 𝐄 (inflatedReference …).

noncomputable def HCPolySupport.HighContrast.Quenched.hatExcessAt {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (r : ℤ) : ℝ

The hatted excess at an absolute scale.

Equations

• HCPolySupport.HighContrast.Quenched.hatExcessAt P q r = ↑d * (HCPolySupport.HighContrast.Quenched.adaptedHattedContrast P q r - 1)

theorem HCPolySupport.HighContrast.Quenched.hatExcessAt_nonneg {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {r : ℤ} (hfin : HasFiniteAdaptedMean P q r) : 0 ≤ hatExcessAt P q r

theorem HCPolySupport.HighContrast.Quenched.contrast_smallness_of_hatExcess {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {t : ℤ} (hfin : HasFiniteAdaptedMean P q t) {delta : ℝ} (hdelta : hatExcessAt P q t ≤ delta) (hdelta9 : delta ≤ 1 / 9) : 6 * (blockContrast (adaptedMean P q t) - 1) ≤ 1

The contrast smallness clause. δ ≤ 1/9 on the hatted excess forces 6(Θ(E_t) − 1) ≤ 1.

theorem HCPolySupport.HighContrast.Quenched.hat_drop_le_hatExcess {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {j p : ℤ} (hfinp : HasFiniteAdaptedMean P q p) : ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p) ≤ hatExcessAt P q j

The drop smallness clause. Every hatted drop is below the excess at its upper scale.