Shift.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Hilbert shifts, their relations, and block operator bounds.

abbrev OAI.Kaplansky.FiberHilbertSum line 18
def OAI.Kaplansky.levelInclusion line 20
theorem OAI.Kaplansky.successor_orthogonal line 24
def OAI.Kaplansky.successorInclusion line 34
Source documentation
Isometric insertion of a zero level at the start of the sum.
```
def successorInclusion : lp (fun j => E (j+1)) 2 →ₗᵢ[ℂ] FiberHilbertSum E :=
…
```
Mentions: OAI.Kaplansky.FiberHilbertSum
def OAI.Kaplansky.forwardShift line 37
theorem OAI.Kaplansky.forwardShift_norm_le line 41
theorem OAI.Kaplansky.forwardShift_single line 49
theorem OAI.Kaplansky.forwardShift_apply_zero line 73
Source documentation
A forward shift has zero output in degree zero.
```
theorem forwardShift_apply_zero (T : ∀ j, E j →L[ℂ] E (j+1)) (hT : ∀ j, ‖T j‖ ≤ 1)
    (f : FiberHilbertSum E) : forwardShift T hT f 0 = 0 := by
…
```
Mentions: OAI.Kaplansky.FiberHilbertSum, OAI.Kaplansky.forwardShift
theorem OAI.Kaplansky.forwardShift_apply_succ line 85
Source documentation
On degree j+1, the forward shift is exactly its j-th block.
```
theorem forwardShift_apply_succ (T : ∀ j, E j →L[ℂ] E (j+1)) (hT : ∀ j, ‖T j‖ ≤ 1)
    (f : FiberHilbertSum E) (j : ℕ) : forwardShift T hT f (j+1) = T j (f j) := by
…
```
Mentions: OAI.Kaplansky.FiberHilbertSum, OAI.Kaplansky.forwardShift

theorem OAI.Kaplansky.forwardShift_adjoint_apply line 100

Source documentation

The adjoint lowers degree, using the adjoint of the actual block.

theorem forwardShift_adjoint_apply (T : ∀ j, E j →L[ℂ] E (j+1)) (hT : ∀ j, ‖T j‖ ≤ 1)
    (f : FiberHilbertSum E) (j : ℕ) :
    (forwardShift T hT).adjoint f j = (T j).adjoint (f (j+1)) := by
…

Mentions: OAI.Kaplansky.FiberHilbertSum, OAI.Kaplansky.forwardShift

theorem OAI.Kaplansky.forwardShift_adjoint_single_zero line 108
theorem OAI.Kaplansky.forwardShift_adjoint_single_succ line 115
theorem OAI.Kaplansky.forwardShift_column line 137
theorem OAI.Kaplansky.forwardShift_row_zero line 145
theorem OAI.Kaplansky.forwardShift_row_succ line 150
theorem OAI.Kaplansky.forwardShift_row_positive line 157
theorem OAI.Kaplansky.block_norm_le_of_column line 193