Metric Diagonal Selection

This is a generic diagonal-selection theorem in a pseudometric space.

Let $X$ be a pseudometric space, let $G:\mathbb N\to\mathbb N\to X$, let $F:\mathbb N\to X$, and let $x\in X$. Assume that for every $n$, $G(n,k)\to F(n)$ as $k\to\infty$, and that $F(n)\to x$ as $n\to\infty$. Then there exists $k:\mathbb N\to\mathbb N$ such that

This provides a reusable diagonalization tool for joint limiting constructions.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem exists_metric_diagonal {X : Type*} [PseudoMetricSpace X]
    (G : ℕ → ℕ → X) (F : ℕ → X) (x : X)
    (hrow : ∀ n : ℕ, Tendsto (G n) atTop (𝓝 (F n))) (houter : Tendsto F atTop (𝓝 x)) :
    ∃ k : ℕ → ℕ, (∀ n, n ≤ k n) ∧ Tendsto k atTop atTop ∧
      Tendsto (fun n => G n (k n)) atTop (𝓝 x)

Module navigation

Module: Analysis/DiagonalSelector.

Source excerpt, lines 18–22 · Frozen source 408915f.