High-contrast homogenization: Provider.Quenched.SmallContrastAccountClauses

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

The remaining account clauses

Beyond the three scaleVariance slots and the mean-drop slot, exists_account_one_step_entry_of_block_at_level asks for three further families of hypotheses. This file produces all of them, grouped by kind:

• the exponent pack — 0 < ρ, ρ < 1, g ≤ ρ at ρ = contrastRho g, and 0 < α ≤ 1/2 at α = recursionAlpha g;
• the Schur pack — the Schur data of the terminal adapted mean, together with the identity that makes the htr clause an equality at eps = hatExcessAt P q t;
• the smallness pack — heps1, hsmall, hdrop and hdropSmall, all from the single scalar hatExcessAt P q k ≤ δ with δ ≤ 1/9.

Only hpos : 0 < eps is left to the caller: at eps = 0 the one-step conclusion is trivial (its right side is nonnegative), so the composition case-splits there.

The exponent pack

The Schur pack

theorem HCPolySupport.HighContrast.Quenched.schur_pack_at_terminal {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} {t : ℤ} (hsym : IsSymmetricBlockMat (adaptedMean P q t)) (hpd : Book.Ch02.BlockPosDef (adaptedMean P q t)) : ∃ (S0 : Mat d) (SStar0 : Mat d) (K0 : Mat d), Matrix.PosDef S0 ∧ Matrix.PosDef SStar0 ∧ toFullBlockMat (adaptedMean P q t) = schurBlock S0 SStar0 K0 ∧ ↑d * (schurHattedContrast S0 SStar0 - 1) = hatExcessAt P q t

The Schur pack at the terminal mean. The Schur data exists, and the account's htr clause holds with equality at eps = hatExcessAt P q t.

The smallness pack

theorem HCPolySupport.HighContrast.Quenched.account_smallness_pack {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hfin : ∀ (k : ℤ), HasFiniteAdaptedMean P q k) {t : ℤ} (hlt : l ≤ t) {delta : ℝ} (hdelta9 : delta ≤ 1 / 9) (hsm : ∀ (k : ℤ), l ≤ k → k ≤ t → hatExcessAt P q k ≤ delta) : hatExcessAt P q t ≤ 1 ∧ 6 * (blockContrast (adaptedMean P q t) - 1) ≤ 1 ∧ ∀ (x y : ℤ), l ≤ x → x ≤ t → ↑d * (adaptedHattedContrast P q x - adaptedHattedContrast P q y) ≤ 1

The full smallness pack. From δ ≤ 1/9 on the hatted excess over the whole range, every remaining scalar clause of the account follows.