High-contrast homogenization: Provider.Quenched.SmallContrastSchurFamilies

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

The Schur families, chosen once

The account core body takes the Schur data as ℕ-indexed families S0 SStar0 K0 : ℕ → Mat d — the choice-free design. schur_data_at_generation supplies the data at each generation individually; this file turns that pointwise existence into the families, and it is the only place in the whole development where choice is introduced deliberately.

Everything downstream of the account core body therefore has a clean provenance for its Classical.choice: it enters here, once, by choose on a generation-indexed family, and nowhere else in the account.

theorem HCPolySupport.HighContrast.Quenched.exists_schur_families {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) (hfin : ∀ (k : ℤ), HasFiniteAdaptedMean P q k) (N₀ : ℕ) : ∃ (S0 : ℕ → Mat d) (SStar0 : ℕ → Mat d) (K0 : ℕ → Mat d), (∀ (m : ℕ), Matrix.PosDef (S0 m)) ∧ (∀ (m : ℕ), Matrix.PosDef (SStar0 m)) ∧ ∀ (m : ℕ), toFullBlockMat (adaptedMean P q (↑N₀ + ↑m)) = schurBlock (S0 m) (SStar0 m) (K0 m)

The Schur families. Pointwise Schur data at every generation, chosen into three ℕ-indexed families with their three properties.