ShiftAlgebra.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The generated Hilbert-shift algebra and its concrete realization.

theorem OAI.Kaplansky.operator_positive_square line 15
Source documentation
Hilbert-space positivity gives an actual square-root factorization.
```
theorem operator_positive_square {a : H →L[ℂ] H} (ha : a.IsPositive) :
    ∃ b : H →L[ℂ] H, a = star b * b :=
…
```
theorem OAI.Kaplansky.operator_positive_spectral line 25
Source documentation
Connect the ordinary operator order to the spectral order of the bounded-product checkpoint.
```
theorem operator_positive_spectral {a : H →L[ℂ] H} (ha : a.IsPositive) : 0 ≤ a := by
…
```
theorem OAI.Kaplansky.forwardShift_row_spectral line 33
theorem OAI.Kaplansky.hilbertShift_generated_relations line 40

theorem OAI.Kaplansky.fiberHilbertSum_nontrivial line 67

Source documentation

A nonzero bottom fiber gives a nonzero ordinary Hilbert sum.

theorem fiberHilbertSum_nontrivial {E : ℕ → Type*} [∀ j, NormedAddCommGroup (E j)]
    [∀ j, InnerProductSpace ℂ (E j)] [∀ j, CompleteSpace (E j)] [Nontrivial (E 0)] :
    Nontrivial (FiberHilbertSum E) :=
…

Mentions: OAI.Kaplansky.FiberHilbertSum

theorem OAI.Kaplansky.source_shift_algebra line 74