HilbertUltraproduct.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.hilbert_tendsto_ultralimit_of_bounded line 16

Source documentation

Bounded scalar families have a genuine ultralimit. No countable completeness or separability hypothesis is used.

theorem hilbert_tendsto_ultralimit_of_bounded {ι : Type u} (ω : Ultrafilter ι)
    {F : Type v} [NormedAddCommGroup F] [ProperSpace F] (f : ι → F)
    (hf : ∃ C : ℝ, ∀ i, ‖f i‖ ≤ C) :
    Tendsto f (ω : Filter ι) (𝓝 (limUnder (ω : Filter ι) f)) := by
…

def OAI.NuclearUltrapower.UltraPreHilbert line 30
Source documentation
A type synonym for bounded Hilbert families, equipped below with the ultralimit semi-inner-product (not with the supremum norm).
```
def UltraPreHilbert {ι : Type u} (E : ι → Type v)
    [∀ i, NormedAddCommGroup (E i)] (_ω : Ultrafilter ι) := lp E ∞
…
```
instance OAI.NuclearUltrapower.UltraPreHilbert.(instance at line 37) line 37
instance OAI.NuclearUltrapower.UltraPreHilbert.(instance at line 38) line 38
def OAI.NuclearUltrapower.UltraPreHilbert.family line 40
theorem OAI.NuclearUltrapower.UltraPreHilbert.family_add line 43
theorem OAI.NuclearUltrapower.UltraPreHilbert.family_smul line 45
theorem OAI.NuclearUltrapower.UltraPreHilbert.inner_tendsto line 48
def OAI.NuclearUltrapower.UltraPreHilbert.core line 57
instance OAI.NuclearUltrapower.UltraPreHilbert.(instance at line 75) line 75
instance OAI.NuclearUltrapower.UltraPreHilbert.(instance at line 78) line 78
theorem OAI.NuclearUltrapower.UltraPreHilbert.inner_def line 80
theorem OAI.NuclearUltrapower.UltraPreHilbert.norm_tendsto line 85
Source documentation
The seminorm is exactly the ultralimit of pointwise norms.
```
theorem norm_tendsto (x : UltraPreHilbert E ω) :
    Tendsto (fun i => ‖family ω x i‖) (ω : Filter ι) (𝓝 ‖x‖) := by
…
```
Mentions: OAI.NuclearUltrapower.UltraPreHilbert, OAI.NuclearUltrapower.UltraPreHilbert.family
abbrev OAI.NuclearUltrapower.HilbertUltraproduct line 97
Source documentation
The Hilbert ultraproduct, implemented as the Hausdorff completion of bounded families for the ultralimit seminorm. This is equivalent to the standard norm-null quotient, but gives completeness without a separate lifting argument.
```
abbrev HilbertUltraproduct {ι : Type u} (E : ι → Type v)
    [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace ℂ (E i)] (ω : Ultrafilter ι) :=
…
```
def OAI.NuclearUltrapower.UltraPreHilbert.mapLinear line 108
Source documentation
Uniformly bounded operator families act on bounded vector families.
```
def mapLinear (T : lp (fun i => E i →L[ℂ] F i) ∞) :
    UltraPreHilbert E ω →ₗ[ℂ] UltraPreHilbert F ω where
…
```
Mentions: OAI.NuclearUltrapower.UltraPreHilbert
theorem OAI.NuclearUltrapower.UltraPreHilbert.family_map line 119
theorem OAI.NuclearUltrapower.UltraPreHilbert.mapLinear_norm_le line 124
Source documentation
Eventual, rather than uniform, bounds suffice after passing to the ultralimit.
```
theorem mapLinear_norm_le (T : lp (fun i => E i →L[ℂ] F i) ∞) (C : ℝ)
    (hT : ∀ᶠ i in (ω : Filter ι), ‖T i‖ ≤ C) (x : UltraPreHilbert E ω) :
    ‖mapLinear ω T x‖ ≤ C * ‖x‖ := by
…
```
Mentions: OAI.NuclearUltrapower.UltraPreHilbert, OAI.NuclearUltrapower.UltraPreHilbert.mapLinear
def OAI.NuclearUltrapower.UltraPreHilbert.mapContinuous line 132
def OAI.NuclearUltrapower.HilbertUltraproduct.map line 146
Source documentation
The induced operator on the completed Hilbert ultraproduct.
```
def map (T : lp (fun i => E i →L[ℂ] F i) ∞) :
    HilbertUltraproduct E ω →L[ℂ] HilbertUltraproduct F ω :=
…
```
Mentions: OAI.NuclearUltrapower.HilbertUltraproduct
theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_coe line 150
theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_norm_le line 156
theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_zero line 180
theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_add line 194
theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_smul line 202
theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_mul line 219
theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_star line 228
def OAI.NuclearUltrapower.HilbertUltraproduct.operatorRep line 241
Source documentation
Bounded operator products and adjoints descend to the Hilbert ultraproduct.
```
def operatorRep : lp (fun i => E i →L[ℂ] E i) ∞ →⋆ₙₐ[ℂ]
    (HilbertUltraproduct E ω →L[ℂ] HilbertUltraproduct E ω) where
…
```
Mentions: OAI.NuclearUltrapower.HilbertUltraproduct
theorem OAI.NuclearUltrapower.HilbertUltraproduct.operatorRep_apply line 250
theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_norm_tendsto line 256
Source documentation
The operator norm on the Hilbert ultraproduct is precisely the ultralimit of coordinate operator norms. In particular no norm information is lost.
```
theorem map_norm_tendsto (T : lp (fun i => E i →L[ℂ] E i) ∞) :
    Tendsto (fun i => ‖T i‖) (ω : Filter ι) (𝓝 ‖map ω T‖) := by
…
```
Mentions: OAI.NuclearUltrapower.HilbertUltraproduct.map
theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_eq_zero_iff line 291
Source documentation
Norm-null families, and only norm-null families, represent zero.
```
theorem map_eq_zero_iff (T : lp (fun i => E i →L[ℂ] E i) ∞) :
    map ω T = 0 ↔ Tendsto (fun i => ‖T i‖) (ω : Filter ι) (𝓝 0) := by
…
```
Mentions: OAI.NuclearUltrapower.HilbertUltraproduct.map