High-contrast homogenization: Provider.Quenched.QuenchedEndgameExponent #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The endgame exponent of the quenched mixing scale #
The concentration exponent μ = d/2 - g of the stopping construction in
ss.random.dirichlet is positive on the whole
admissible range and doubles to the stretched exponent d - 2g of the
homogenization-scale tail. This file records that identification and delivers
the coupled mixing-scale witness with the exponent written in the shape the
homogenization statement uses.
theorem
HCPolySupport.HighContrast.Quenched.exists_coupled_mixingScale_at_exponent
{Ω : Type u_1}
[MeasurableSpace Ω]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{nstar qfb b : ℕ}
{R B F : ℕ → Ω → ℝ}
{theta mu eta cd delta Cblk : ℝ}
(htheta : 0 < theta)
(hmu : 0 < mu)
(heta : eta = 2 * mu)
(hcd : 0 < cd)
(hdelta : 0 < delta)
(hCblk : 0 < Cblk)
(hFmeas : ∀ (n : ℕ), Measurable (F n))
(hRtail : ∀ (n q : ℕ), nstar ≤ n → P.real {ω : Ω | 3 ^ (n + q + b) < R n ω} ≤ Real.exp (-(cd * 3 ^ (2 * mu * ↑q))))
(hBdecay :
∀ᵐ (ω : Ω) ∂P, ∀ (m : ℕ), nstar ≤ m → B m ω ≤ Cblk * delta * 3 ^ (-theta * (↑m - ↑(stoppingGeneration nstar qfb R m ω) - ↑nstar)))
(hFsum : ∀ᵐ (ω : Ω) ∂P, ∀ (k : ℕ), HasSum (fun (j : ℕ) => 3 ^ (theta / 2 * ↑j) * B (k + j) ω) (F k ω))
{N0 : ℕ}
{Bconst : ℝ}
(hstar : nstar ≤ N0)
(hBconst : 1 ≤ Bconst)
(hN0low : ↑qfb + ↑b + 1 + rowSplitOffset theta Cblk ≤ ↑N0 - ↑nstar)
(hN0gain : Real.log 2 ≤ cd * 3 ^ (2 * mu * (↑N0 - ↑nstar - badTailOffset theta Cblk qfb b)) * (3 ^ (mu / 2) - 1))
(hN0abs : 2 * Real.log 4 ≤ cd * 3 ^ (2 * mu * (↑N0 - ↑nstar - badTailOffset theta Cblk qfb b)))
(hBrel : 3 ^ (2 * mu * (↑nstar + badTailOffset theta Cblk qfb b - ↑N0)) ≤ cd / 2 * Bconst ^ (2 * mu))
:
∃ (Amix : ℝ) (Rmix : Ω → ℝ),
Amix = 3 * 3 ^ N0 * Bconst ∧ 1 ≤ Amix ∧ Measurable Rmix ∧ (∀ (ω : Ω), 1 ≤ Rmix ω) ∧ (∀ (t : ℝ), 1 ≤ t → P.real {ω : Ω | 2 * t ≤ Rmix ω} ≤ Real.exp (-1 * t ^ eta)) ∧ (∀ (n : ℕ), MeasurableSet (rowBadEvent delta F n)) ∧ (∀ (n : ℕ) (ω : Ω), ω ∈ rowBadEvent delta F n ↔ delta ≤ F n ω) ∧ ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), Amix * Rmix ω ≤ 3 ^ n → ω ∉ rowBadEvent delta F n
The coupled mixing-scale witness with the stretched exponent written as the homogenization statement writes it.