High-contrast homogenization: Provider.Quenched.SmallContrastOneStepFamilySplit #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The burn-split one-step family at every admissible base index #
The recursion family with the slot family at supplyMscSplit d E under
the burn-in condition — the choice function quantified before the
generation.
theorem
HCPolySupport.HighContrast.Quenched.exists_one_step_family_of_block_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 a growing window, at every admissible base index. The choice function is quantified before the generation.