High-contrast homogenization: Provider.Quenched.SmallContrastOneStepSlotsSplit #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The burn-split one-step estimate with its slots #
The released one-step estimate with the slot family at the burn-split
supply supplyMscSplit d E; the weak-cap branch keeps its availability
threshold unchanged.
theorem
HCPolySupport.HighContrast.Quenched.exists_one_step_with_slots_of_block_at_level_conv_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 →
∀ {s t : ℤ},
s ≤ t →
t = s + ↑H →
lAl ≤ s →
∀ (Hw : ℕ),
lAl ≤ t - ↑Hw →
∀ {sKw : ℤ},
growthBar K ≤ 3 ^ sKw →
sKw ≤ t - ↑Hw →
sourceMomentTwo K ≤ 3 ^ (t - ↑Hw + ↑(Gacc + 1) - sKw) →
∀ (M : ℕ),
1 + 2 * ↑(2 + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (2 + M) ≤ 3 ^ (↑M * ↑(t - ↑Hw + ↑(Gacc + 1) - 1 - sKw)) →
∀ {jb : ℤ},
t - ↑Hw ≤ jb →
jb ≤ t →
∀ {delta : ℝ},
0 ≤ delta →
delta ≤ 1 / 9 →
(∀ (k : ℤ),
lAl ≤ k →
k ≤ t →
hatExcessAt P
(roundedGrid lAl mAl)
k ≤ delta) →
∀ {Csub : ℝ}, ⋯
The one-step estimate with slots, at the caller's mean conversion.