UltrapowerConstants.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Constant Hilbert vectors retain both their norm and the action of every constant bounded operator inside the actual Hilbert ultrapower.

def OAI.KadisonSimilarity.boundedConstant line 17
Source documentation
A constant bounded family, with the ordinary supremum-norm domain.
```
def boundedConstant {E : Type*} [NormedAddCommGroup E] (x : E) : lp (fun _ : ι => E) ∞ :=
…
```
theorem OAI.KadisonSimilarity.boundedConstant_apply line 20
def OAI.KadisonSimilarity.constantPreHilbert line 24
Source documentation
The ultralimit seminorm of a constant family is its original norm.
```
def constantPreHilbert (ω : Ultrafilter ι) : H →ₗᵢ[ℂ] UltraPreHilbert (fun _ : ι => H) ω where
…
```
def OAI.KadisonSimilarity.constantHilbertInclusion line 33
Source documentation
The isometric constant-vector inclusion in the completed Hilbert ultrapower.
```
def constantHilbertInclusion (ω : Ultrafilter ι) :
    H →ₗᵢ[ℂ] HilbertUltraproduct (fun _ : ι => H) ω :=
…
```
theorem OAI.KadisonSimilarity.constantHilbertInclusion_apply line 38
theorem OAI.KadisonSimilarity.map_constant_operator line 45
Source documentation
The coordinatewise action of a fixed operator preserves the constant subspace.
```
theorem map_constant_operator (ω : Ultrafilter ι) (T : H →L[ℂ] H) (x : H) :
    HilbertUltraproduct.map ω (boundedConstant T) (constantHilbertInclusion ω x) =
      constantHilbertInclusion ω (T x) := by
…
```
Mentions: OAI.KadisonSimilarity.boundedConstant, OAI.KadisonSimilarity.constantHilbertInclusion
theorem OAI.KadisonSimilarity.norm_map_constant_operator line 54
Source documentation
No operator norm is lost on a constant family.
```
theorem norm_map_constant_operator (ω : Ultrafilter ι) (T : H →L[ℂ] H) :
    ‖HilbertUltraproduct.map ω (boundedConstant T)‖ = ‖T‖ :=
…
```
Mentions: OAI.KadisonSimilarity.boundedConstant
theorem OAI.KadisonSimilarity.compression_map_constant_operator line 61
Source documentation
Compressing the ultrapower operator back to the constant subspace recovers the original operator exactly.
```
theorem compression_map_constant_operator (ω : Ultrafilter ι) (T : H →L[ℂ] H) :
    (constantHilbertInclusion (H := H) ω).toContinuousLinearMap.adjoint.comp
…
```
Mentions: OAI.KadisonSimilarity.constantHilbertInclusion