UltraRealLimit.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Real ultralimits of bounded sequences

Every bounded real sequence converges along an ultrafilter, by compactness of a closed real interval. All identities below use this convergence or an explicitly given limit, so they do not depend on the fallback value of limUnder.

def OAI.Tingley.RealSeqBounded line 24
Source documentation
A real sequence has a uniform absolute-value bound.
```
def RealSeqBounded (f : ℕ → ℝ) : Prop :=
…
```
theorem OAI.Tingley.RealSeqBounded.exists_nonneg_bound line 31
theorem OAI.Tingley.RealSeqBounded.const line 36
theorem OAI.Tingley.RealSeqBounded.add line 39
theorem OAI.Tingley.RealSeqBounded.neg line 45
theorem OAI.Tingley.RealSeqBounded.sub line 50
theorem OAI.Tingley.RealSeqBounded.const_mul line 54
theorem OAI.Tingley.RealSeqBounded.abs line 61
def OAI.Tingley.realULim line 70
Source documentation
The chosen real limit along an ultrafilter. Use tendsto_realULim to establish that this value is a limit for a bounded sequence.
```
def realULim (U : Ultrafilter ℕ) (f : ℕ → ℝ) : ℝ :=
…
```
theorem OAI.Tingley.tendsto_realULim line 76
Source documentation
Bounded real sequences converge along every ultrafilter.
```
theorem tendsto_realULim (U : Ultrafilter ℕ) (hf : RealSeqBounded f) :
    Tendsto f (U : Filter ℕ) (𝓝 (realULim U f)) := by
…
```
Mentions: OAI.Tingley.RealSeqBounded, OAI.Tingley.realULim
theorem OAI.Tingley.realULim_eq_of_tendsto line 88
Source documentation
A known limit determines the chosen ultralimit, without a boundedness premise.
```
theorem realULim_eq_of_tendsto (U : Ultrafilter ℕ) {a : ℝ}
    (h : Tendsto f (U : Filter ℕ) (𝓝 a)) : realULim U f = a :=
…
```
Mentions: OAI.Tingley.realULim
theorem OAI.Tingley.realULim_const line 93
theorem OAI.Tingley.realULim_add line 97
theorem OAI.Tingley.realULim_neg line 102
theorem OAI.Tingley.realULim_sub line 106
theorem OAI.Tingley.realULim_const_mul line 111
theorem OAI.Tingley.realULim_abs line 115

theorem OAI.Tingley.realULim_le_realULim line 120

Source documentation

Eventual inequalities pass to the limits of bounded real sequences.

theorem realULim_le_realULim (U : Ultrafilter ℕ) (hf : RealSeqBounded f)
    (hg : RealSeqBounded g) (h : ∀ᶠ n in (U : Filter ℕ), f n ≤ g n) :
    realULim U f ≤ realULim U g :=
…

Mentions: OAI.Tingley.RealSeqBounded, OAI.Tingley.realULim

theorem OAI.Tingley.realULim_le_of_eventually_le line 125
theorem OAI.Tingley.le_realULim_of_eventually_le line 129
def OAI.Tingley.freeUltrafilter line 135
Source documentation
The actual free ultrafilter used for the bounded-sequence quotient.
```
def freeUltrafilter : Ultrafilter ℕ := Filter.hyperfilter ℕ
```
theorem OAI.Tingley.freeUltrafilter_le_cofinite line 137
theorem OAI.Tingley.freeUltrafilter_le_atTop line 141
theorem OAI.Tingley.not_mem_freeUltrafilter_of_finite line 144

theorem OAI.Tingley.tendsto_freeUltrafilter_of_tendsto_atTop line 149

Source documentation

Ordinary sequential convergence also holds along the fixed free ultrafilter.

theorem tendsto_freeUltrafilter_of_tendsto_atTop {α : Type*} [TopologicalSpace α]
    {a : ℕ → α} {x : α} (h : Tendsto a atTop (𝓝 x)) :
    Tendsto a (freeUltrafilter : Filter ℕ) (𝓝 x) :=
…

Mentions: OAI.Tingley.freeUltrafilter

theorem OAI.Tingley.realULim_freeUltrafilter_eq_of_tendsto_atTop line 154