Limit notation : convergence definition

Stream: Is there code for X?

[Bashar Hamade]

I would like to write something like :

Given $\lim_{k \to \infty} \|A_k\| = l$, where $l < r < 1$, there exists some $N$ such that for all $k > N$, $\|A_k\| < r$.

is there some definition that yields me the definitions with the notation :

for all $$k > N$$

The basic Filter definitions do not seem to provide such intuitive definition

[Edward van de Meent]

are you looking for this?

import Mathlib
variable {A : ℕ → ℝ} (r : ℝ)
#check ∀ᶠ k in (Filter.atTop (α := ℕ)), |A k| < r

[Bashar Hamade]

Edward van de Meent said:

are you looking for this?

import Mathlib
variable {A : ℕ → ℝ} (r : ℝ)
#check ∀ᶠ k in (Filter.atTop (α := ℕ)), |A k| < r

yeah that seems good, but I am more interested in like switching between a filter.limsup notation into such notations , for example to prove this :

import Mathlib

variable {R : Type*} [NormedField R]
variable {A : Type*}
variable {n : ℕ}

open scoped ComplexOrder



theorem convergence  {A : Type*} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A]
  (a : A) (h : Filter.limsup (fun n : ℕ ↦ (‖a ^ n‖₊ : ENNReal) ) Filter.atTop < 1)  :
∃ (r : ENNReal) (N : ℕ), 0 < r ∧ r < 1 ∧ ∀ (k : ℕ), N < k → (‖a ^ k‖₊ : ENNReal)  < r := by

  sorry

[Bashar Hamade]

I feel like there should be some somewhat equivalent theorems that can finish the proof or can write something similar instead of proving it from scratch

[Aaron Liu]

Why do you have to get values out?

[Bashar Hamade]

it is part of a bigger proof , what I mainly need is actually to prove :

$$\lim_{n \to \infty} \|A^n\|^{1/n} < 1 \implies \|A^n\| \to 0$$

[Aaron Liu]

I don't see why you would need to get a number out to do that

[Terence Tao]

perhaps docs#Filter.eventually_lt_of_limsup_lt will be helpful?

[Terence Tao]

I got that link (and other potentially useful tools) from this Loogle search:

[Terence Tao]

@loogle Filter.limsup, ?a < ?b

[loogle]

:search: Filter.eventually_lt_of_limsup_lt, Filter.frequently_lt_of_lt_limsup, and 7 more

[Aaron Liu]

Terence Tao said:

perhaps docs#Filter.eventually_lt_of_limsup_lt will be helpful?

This one probably won't be enough on its own

[Aaron Liu]

you also need to do some halving

[Terence Tao]

docs#exists_between should take care of that