High-contrast homogenization: Provider.Quenched.QuenchedRowSeries

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

The weighted row series and its bad events

The endgame weights the block rows of the successive generations by a growing triadic factor and stops at the first generation whose weighted tail series stays below a fixed threshold (e.random.adapted.sum, e.random.final.scale). This file fixes the resulting bad events, proves that a bad event forces one later generation map to be large, and turns the resulting union bound into a single stretched-exponential estimate for one generation.

The bad events of the weighted row series

def HCPolySupport.HighContrast.Quenched.rowBadEvent {Ω : Type u_1} (delta : ℝ) (F : ℕ → Ω → ℝ) (n : ℕ) : Set Ω

The bad event at a generation: the weighted tail series of the block rows reaches the threshold.

Equations

• HCPolySupport.HighContrast.Quenched.rowBadEvent delta F n = {ω : Ω | delta ≤ F n ω}

theorem HCPolySupport.HighContrast.Quenched.measurableSet_rowBadEvent {Ω : Type u_1} [MeasurableSpace Ω] {F : ℕ → Ω → ℝ} (hF : ∀ (n : ℕ), Measurable (F n)) (delta : ℝ) (n : ℕ) : MeasurableSet (rowBadEvent delta F n)

The bad events are measurable as soon as the tail series is.

The deterministic split offset

noncomputable def HCPolySupport.HighContrast.Quenched.rowSplitOffset (theta Cblk : ℝ) : ℝ

The deterministic offset that absorbs the summable weights and the row constant when the weighted series is split across generations.

Equations

• HCPolySupport.HighContrast.Quenched.rowSplitOffset theta Cblk = -Real.logb 3 ((1 - 3 ^ (-theta / 4)) / (2 * Cblk)) / theta

theorem HCPolySupport.HighContrast.Quenched.rpow_neg_div_lt_one {theta : ℝ} (htheta : 0 < theta) : 3 ^ (-theta / 4) < 1

The triadic weight at the base of the split offset is below one.

theorem HCPolySupport.HighContrast.Quenched.rpow_neg_mul_rowSplitOffset {theta Cblk : ℝ} (htheta : 0 < theta) (hCblk : 0 < Cblk) : 3 ^ (-theta * rowSplitOffset theta Cblk) = (1 - 3 ^ (-theta / 4)) / (2 * Cblk)

The split offset is the exact triadic exponent of the absorbed constant.

A bad row series forces a large generation map

theorem HCPolySupport.HighContrast.Quenched.exists_lt_stoppingGeneration_of_rowBadEvent {Ω : Type u_1} {nstar qfb : ℕ} {R B F : ℕ → Ω → ℝ} {theta delta Cblk : ℝ} (htheta : 0 < theta) (hdelta : 0 < delta) (hCblk : 0 < Cblk) {n : ℕ} (hn : nstar ≤ n) {ω : Ω} (hBdecay : ∀ (m : ℕ), nstar ≤ m → B m ω ≤ Cblk * delta * 3 ^ (-theta * (↑m - ↑(stoppingGeneration nstar qfb R m ω) - ↑nstar))) (hsum : HasSum (fun (j : ℕ) => 3 ^ (theta / 2 * ↑j) * B (n + j) ω) (F n ω)) (hbad : ω ∈ rowBadEvent delta F n) : ∃ (j : ℕ), ↑j / 4 + (↑n - ↑nstar) - rowSplitOffset theta Cblk < ↑(stoppingGeneration nstar qfb R (n + j) ω)

On the summability event a bad weighted row series forces the generation map of one later generation to exceed the split threshold.