Show tails of a convergent sequence converge

Stream: new members

[mdnestor]

Hi, I am trying to show the tails of a convergent sequence also converge, any ideas? The mathlib docs on theorems about filters is greek to me :)

import Mathlib.Topology.Basic

def converge [TopologicalSpace X] (a: Nat → X) (x: X): Prop :=
  Filter.Tendsto a Filter.atTop (nhds x)

theorem tails_converge [TopologicalSpace X] {a: Nat → X} {x: X} (h: converge a x): ∀ t: Nat, converge (a ∘ (fun n => n + t)) x := by
  sorry

[mdnestor]

This is pretty easy using standard topological definition of convergent sequence but I also cannot find the equivalence to the filter definition

[Jireh Loreaux]

@loogle HAdd.hAdd, Nat, Filter.Tendsto, Filter.atTop

[loogle]

:search: Filter.tendsto_add_atTop_nat, Filter.tendsto_add_atTop_iff_nat, and 62 more

[Jireh Loreaux]

How about docs#Filter.Tendsto.comp + docs#Filter.tendsto_add_atTop_nat ?

[Jireh Loreaux]

You should read #mil if you don't understand filters.

[Jireh Loreaux]

Namely, starting with Section 9.1

[mdnestor]

So the theorem I was looking for is tendsto_atTop_nhds which is the equivalence between the filter definition of convergent sequence and the standard topological definition. Here is complete proof.

import Mathlib.Topology.Basic

def converge [TopologicalSpace X] (a: Nat → X) (x: X): Prop :=
  Filter.Tendsto a Filter.atTop (nhds x)

theorem tails_converge [TopologicalSpace X] {a: Nat → X} {x: X} (h: converge a x): ∀ t: Nat, converge (a ∘ (fun n => n + t)) x := by
  intro t
  rw [converge, tendsto_atTop_nhds]
  have h1 := tendsto_atTop_nhds.mp h
  intro U hx hU
  obtain ⟨N, hN⟩ := h1 U hx hU
  exists N - t
  intro n h2
  simp at h2
  exact hN (n + t) h2

[Luigi Massacci]

This way you are doing the proof "manually" (which might be what you want of course), but the two lemmas Jireh suggested to you should suffice to one-line it