High-contrast homogenization: Provider.Quenched.SmallContrastOneStepEntryIsotropyAtLevel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The account's one-step entry estimate at a released split level #
The hub applied at the released caps: the weak slot is the released sharp weak value and every other slot is the pinned one.
theorem
HCPolySupport.HighContrast.Quenched.exists_account_one_step_entry_of_block_at_level
(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 →
∀ {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 + ↑(Gacc + 1) - sKw) →
(∀ (k : ℤ),
lAl ≤ k →
k ≤ t →
HasFiniteAdaptedMean P (roundedGrid lAl mAl) k ∧ Book.Ch02.BlockPosDef
(adaptedMean P (roundedGrid lAl mAl) k)) →
∀ {S0 SStar0 K0 : Mat d},
Matrix.PosDef S0 →
Matrix.PosDef SStar0 →
toFullBlockMat
(adaptedMean P (roundedGrid lAl mAl) t) = schurBlock S0 SStar0 K0 →
∀ {eps : ℝ},
0 < eps →
eps ≤ 1 →
↑d * (schurHattedContrast S0 SStar0 - 1) ≤ eps →
6 * (blockContrast
(adaptedMean P
(roundedGrid lAl mAl) t) - 1) ≤ 1 →
↑d * (adaptedHattedContrast P
(roundedGrid lAl mAl) s - adaptedHattedContrast P
(roundedGrid lAl mAl) t) ≤ 1 →
⋯ → ⋯
The account's one-step entry estimate, at a released split level.