UltraNormed.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

Bounded sequences with the ultralimit seminorm

The carrier below is a fresh wrapper, not the bounded submodule with its inherited product topology. Only algebra is transported to the wrapper. Its topology is then constructed from the ultralimit seminorm. The separation quotient therefore identifies zero ultradistance, not eventual equality.

def OAI.Tingley.boundedSequenceSubmodule line 27
Source documentation
The algebraic submodule of uniformly bounded sequences.
```
def boundedSequenceSubmodule : Submodule ℝ (ℕ → X) where
…
```
structure OAI.Tingley.UltraSequence line 41
Source documentation
A fresh carrier on which only the ultralimit topology will be installed.
```
structure UltraSequence (U : Ultrafilter ℕ) (X : Type u)
    [NormedAddCommGroup X] [NormedSpace ℝ X] where
…
```
def OAI.Tingley.UltraSequence.algebraEquiv line 50
Source documentation
Algebraic identification; it transports no topology.
```
def algebraEquiv : UltraSequence U X ≃ boundedSequenceSubmodule X where
…
```
Mentions: OAI.Tingley.UltraSequence, OAI.Tingley.boundedSequenceSubmodule
instance OAI.Tingley.UltraSequence.instAddCommGroup line 56
instance OAI.Tingley.UltraSequence.instModule line 59
instance OAI.Tingley.UltraSequence.instCoeFun line 63
theorem OAI.Tingley.UltraSequence.ext line 68
def OAI.Tingley.UltraSequence.ofBounded line 76
Source documentation
Construct a sequence from an actual uniform norm bound.
```
def ofBounded (U : Ultrafilter ℕ) (a : ℕ → X)
    (ha : ∃ B : ℝ, 0 ≤ B ∧ ∀ n, ‖a n‖ ≤ B) : UltraSequence U X :=
…
```
Mentions: OAI.Tingley.UltraSequence
theorem OAI.Tingley.UltraSequence.ofBounded_apply line 80
theorem OAI.Tingley.UltraSequence.zero_apply line 84
theorem OAI.Tingley.UltraSequence.add_apply line 86
theorem OAI.Tingley.UltraSequence.neg_apply line 89
theorem OAI.Tingley.UltraSequence.sub_apply line 91
theorem OAI.Tingley.UltraSequence.smul_apply line 94
theorem OAI.Tingley.UltraSequence.bounded line 97
theorem OAI.Tingley.UltraSequence.norm_bounded line 100
def OAI.Tingley.UltraSequence.ultranorm line 105
Source documentation
The actual ultralimit of coordinate norms.
```
def ultranorm (a : UltraSequence U X) : ℝ := realULim U (fun n => ‖a n‖)
```
Mentions: OAI.Tingley.UltraSequence, OAI.Tingley.realULim
theorem OAI.Tingley.UltraSequence.ultranorm_add_le line 107
theorem OAI.Tingley.UltraSequence.ultranorm_smul line 114
def OAI.Tingley.UltraSequence.seminorm line 122
Source documentation
The proved seminorm; no bounded-vector convergence is asserted.
```
def seminorm : Seminorm ℝ (UltraSequence U X) :=
…
```
Mentions: OAI.Tingley.UltraSequence
instance OAI.Tingley.UltraSequence.instSeminormedAddCommGroup line 125
instance OAI.Tingley.UltraSequence.instNormedSpace line 128
theorem OAI.Tingley.UltraSequence.norm_eq_realULim line 133
def OAI.Tingley.UltraSequence.constant line 137
Source documentation
Constant bounded sequences.
```
def constant (U : Ultrafilter ℕ) (x : X) : UltraSequence U X :=
…
```
Mentions: OAI.Tingley.UltraSequence
theorem OAI.Tingley.UltraSequence.constant_apply line 140
abbrev OAI.Tingley.UltraQuotient line 146
Source documentation
The normed space obtained by identifying sequences at zero ultradistance.
```
abbrev UltraQuotient (U : Ultrafilter ℕ) (X : Type u)
    [NormedAddCommGroup X] [NormedSpace ℝ X] :=
…
```
def OAI.Tingley.classOf line 153
Source documentation
Projection to the zero-ultranorm quotient.
```
def classOf (a : UltraSequence U X) : UltraQuotient U X := SeparationQuotient.mk a
```
Mentions: OAI.Tingley.UltraSequence, OAI.Tingley.UltraQuotient
theorem OAI.Tingley.classOf_surjective line 155
theorem OAI.Tingley.classOf_zero line 159
theorem OAI.Tingley.classOf_add line 161
theorem OAI.Tingley.classOf_neg line 164
theorem OAI.Tingley.classOf_sub line 166
theorem OAI.Tingley.classOf_smul line 169
theorem OAI.Tingley.norm_classOf line 172
theorem OAI.Tingley.norm_sub_classOf line 175
theorem OAI.Tingley.classOf_eq_iff line 180
def OAI.Tingley.constantEmbedding line 185
Source documentation
Constant sequences embed the original space isometrically and linearly.
```
def constantEmbedding : X →ₗᵢ[ℝ] UltraQuotient U X where
…
```
Mentions: OAI.Tingley.UltraQuotient
theorem OAI.Tingley.constantEmbedding_apply line 198
instance OAI.Tingley.ultraQuotient_nontrivial line 201
abbrev OAI.Tingley.UltraCompletion line 205
Source documentation
The actual Banach completion of the normed ultralimit quotient.
```
abbrev UltraCompletion (U : Ultrafilter ℕ) (X : Type u)
    [NormedAddCommGroup X] [NormedSpace ℝ X] :=
…
```
instance OAI.Tingley.ultraCompletion_nontrivial line 209