A metastable dominated convergence theorem

Jeremy Avigad, Edward T Dean, Jason Rute

We prove the equivalence between the two first displayed equations mentioned on page 2.

def P₁ (a : ℕ → ℝ) : Prop

Equations

• P₁ a = ∀ ε > 0, ∃ (m : ℕ), ∀ n ≥ m, ∀ n' ≥ m, |a n - a n'| < ε

def P₂ (a : ℕ → ℝ) : Prop

Equations

• P₂ a = ∀ ε > 0, ∀ (F : ℕ → ℕ), ∃ (m : ℕ), ∀ n ∈ Set.Icc m (F m), ∀ n' ∈ Set.Icc m (F m), |a n - a n'| < ε

theorem metastableEquiv₁ (a : ℕ → ℝ) : P₁ a → P₂ a

theorem metastableAux {a : ℕ → ℝ} {ε : ℝ} {m : ℕ} (h : ∃ n ≥ m, ∃ n' ≥ m, ε ≤ |a n - a n'|) : ∃ (k : ℕ), ∃ n ∈ Set.Icc m k, ∃ n' ∈ Set.Icc m k, ε ≤ |a n - a n'|

theorem metastableEquiv₂ (a : ℕ → ℝ) : P₂ a → P₁ a