High-contrast homogenization: Provider.Quenched.SmallContrastOneStepFamilyAtIsotropySplit

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

The burn-split one-step family at the isotropy carriers

The Tier-A-discharged family producer at the burn-split supply supplyMscSplit d E: the isotropy pack's discharges as given, the mesoscale ceiling and burn depth as hypotheses, the slot family dimensional up to κ_𝐄.

theorem HCPolySupport.HighContrast.Quenched.exists_one_step_family_at_isotropy_var_at_level_conv_family_split (d : ℕ) (hd : 2 ≤ d) : ∃ (Cpre : ℝ) (H : ℕ) (eta : ℝ), 1 ≤ Cpre ∧ 4 ≤ H ∧ 0 < eta ∧ ∀ {g : ℝ}, g ∈ Set.Ico 0 1 → ∀ {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ}, CoarseEllipticityDagger P g E Ψ K S → IsStationaryLaw P → ∀ {lAl : ℤ}, ↑(kZero d) ≤ lAl → ∀ {Cd : ℝ}, max 1 (12 * ↑d * √↑d) ≤ Cd → ∀ {mAl : Mat d}, Matrix.PosDef mAl → IsRoundedGrid lAl (roundedGrid lAl mAl) → ∀ {Gacc : ℕ}, ‖roundedGrid lAl mAl‖ * √↑d ≤ 3 ^ Gacc → boundaryConst Cd g mAl ≤ 3 ^ (Gacc + 1) → (∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), S a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - 2 * ↑(Gacc + 1) - ↑k) 0)) E)) → ∀ {rho : ℝ}, 0 < rho → rho < 1 → g ≤ rho → ∀ (Hw : ℕ → ℕ) {sKw : ℤ}, growthBar K ≤ 3 ^ sKw → ∀ {delta : ℝ}, 0 ≤ delta → delta ≤ 1 / 9 → (∀ (k : ℤ), lAl ≤ k → hatExcessAt P (roundedGrid lAl mAl) k ≤ delta) → ∀ {Csub : ℝ}, 0 < Csub → (∀ (j' p' : ℤ), lAl ≤ j' → j' ≤ p' → ∃ (Z : Finset (Fin d → ℤ)), ↑Z = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid lAl mAl) j' w ∈ adaptedCell (roundedGrid lAl mAl) p'} ∧ Z.card = 3 ^ (d * (p' - j').toNat) ∧ Z.Nonempty ∧ lqSchattenSize P 2 (fun (a : CoeffSpace d) => ⋯) (adaptedMean P (roundedGrid lAl mAl) p') ≤ ENNReal.ofReal (Csub * ↑Z.card ^ (-2⁻¹)) * lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (coarseBlock (adaptedCell (roundedGrid lAl mAl) j') a) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p')) → ∀ {N₀ ns : ℕ}, H + 1 ≤ ns → lAl ≤ ↑N₀ + ↑(ns - H) → (∀ (n : ℕ), ns ≤ n → lAl ≤ ↑N₀ + ↑n - ↑(Hw n)) → (∀ (n : ℕ), ns ≤ n → sKw ≤ ↑N₀ + ↑n - ↑(Hw n)) → (∀ (n : ℕ), ns ≤ n → sourceMomentTwo K ≤ 3 ^ ⋯) → ∀ (M : ℕ), (∀ (n : ℕ), ns ≤ n → ⋯) → ∀ (jb : ℕ → ℕ), ⋯ → ⋯

The one-step family at the isotropy carriers, at every admissible base index. The recursion family as the print proves it (every depth in the window), at the pack's own carriers; the shifted instantiation is the member jb := shiftedBaseIndex ns.

theorem HCPolySupport.HighContrast.Quenched.exists_one_step_family_at_isotropy_var_at_level_conv_family_min (d : ℕ) (hd : 2 ≤ d) : ∃ (Cpre : ℝ) (H : ℕ) (eta : ℝ), 1 ≤ Cpre ∧ 4 ≤ H ∧ 0 < eta ∧ ∀ {g : ℝ}, g ∈ Set.Ico 0 1 → ∀ {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ}, CoarseEllipticityDagger P g E Ψ K S → IsStationaryLaw P → ∀ {lAl : ℤ}, ↑(kZero d) ≤ lAl → ∀ {Cd : ℝ}, max 1 (12 * ↑d * √↑d) ≤ Cd → ∀ {mAl : Mat d}, Matrix.PosDef mAl → IsRoundedGrid lAl (roundedGrid lAl mAl) → ∀ {Gacc : ℕ}, ‖roundedGrid lAl mAl‖ * √↑d ≤ 3 ^ Gacc → boundaryConst Cd g mAl ≤ 3 ^ (Gacc + 1) → (∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), S a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - 2 * ↑(Gacc + 1) - ↑k) 0)) E)) → ∀ {rho : ℝ}, 0 < rho → rho < 1 → g ≤ rho → ∀ {sKw : ℤ}, growthBar K ≤ 3 ^ sKw → ∀ {delta : ℝ}, 0 ≤ delta → delta ≤ 1 / 9 → (∀ (k : ℤ), lAl ≤ k → hatExcessAt P (roundedGrid lAl mAl) k ≤ delta) → ∀ {Csub : ℝ}, 0 < Csub → (∀ (j' p' : ℤ), lAl ≤ j' → j' ≤ p' → ∃ (Z : Finset (Fin d → ℤ)), ↑Z = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid lAl mAl) j' w ∈ adaptedCell (roundedGrid lAl mAl) p'} ∧ Z.card = 3 ^ (d * (p' - j').toNat) ∧ Z.Nonempty ∧ lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub ⋯ (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p') ≤ ENNReal.ofReal (Csub * ↑Z.card ^ (-2⁻¹)) * lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (coarseBlock (adaptedCell (roundedGrid lAl mAl) j') a) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p')) → ∀ {N₀ ns : ℕ}, H + 1 ≤ ns → lAl ≤ ↑N₀ + ↑(ns - H) → (∀ (n : ℕ), ns ≤ n → lAl ≤ ↑N₀ + ↑n - ↑(n - ns)) → (∀ (n : ℕ), ns ≤ n → sKw ≤ ↑N₀ + ↑n - ↑(n - ns)) → (∀ (n : ℕ), ns ≤ n → sourceMomentTwo K ≤ 3 ^ (↑N₀ + ↑n - ↑(n - ns) + ↑(Gacc + 1) - sKw)) → ∀ (M : ℕ), (∀ (n : ℕ), ns ≤ n → ⋯ ≤ ⋯) → ∀ {sigma cEnt : ℝ}, refContrast E - 1 ≤ sigma → 0 ≤ sigma → ⋯

The split one-step family at the cadence consumer's minimum base. The generation window is specialized to n - ns, the base index to min n m, and the zero-excess endpoint is included.