HilbertRows.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Products of operator rows on finite Hilbert sums

def OAI.KadisonKastler.operatorRow line 21
theorem OAI.KadisonKastler.operatorRow_apply line 26
theorem OAI.KadisonKastler.norm_operatorRow_apply line 29
theorem OAI.KadisonKastler.norm_operatorRow_le line 36
theorem OAI.KadisonKastler.norm_fibreRow_apply line 46
Source documentation
Repeating an operator row on each fibre does not enlarge its norm.
```
theorem norm_fibreRow_apply (D : J → H →L[ℂ] H)
    (x : Generator.FiniteHilbert (I × J) H) :
    ‖WithLp.toLp 2 (fun i => ∑ j, D j (x (i, j)))‖ ≤ ‖operatorRow D‖ * ‖x‖ := by
…
```
Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.operatorRow
theorem OAI.KadisonKastler.norm_operatorRow_products_le line 60
Source documentation
Creating another letter multiplies the row bound, even when the letters act on the same Hilbert space and do not commute.
```
theorem norm_operatorRow_products_le (C : I → H →L[ℂ] H) (D : J → H →L[ℂ] H) :
    ‖operatorRow (fun ij : I × J => C ij.1 * D ij.2)‖ ≤
      ‖operatorRow C‖ * ‖operatorRow D‖ := by
…
```
Mentions: OAI.KadisonKastler.operatorRow
theorem OAI.KadisonKastler.norm_operatorRow_comp_le line 77
Source documentation
Restricting a row to an injective selection of labels is contractive.
```
theorem norm_operatorRow_comp_le (C : I → H →L[ℂ] H) (f : J → I)
    (hf : Function.Injective f) : ‖operatorRow (C ∘ f)‖ ≤ ‖operatorRow C‖ := by
…
```
Mentions: OAI.KadisonKastler.operatorRow
theorem OAI.KadisonKastler.norm_operatorRow_reindex line 98
def OAI.KadisonKastler.tupleOperatorProduct line 104

theorem OAI.KadisonKastler.norm_tupleOperatorRow_le line 109

Source documentation

Iterated creation rows have the product of the one-letter row bounds.

theorem norm_tupleOperatorRow_le {α : Type*} [Fintype α] (n : ℕ)
    (C : Fin n → α → H →L[ℂ] H) {c : ℝ} (hc : 0 ≤ c)
    (hC : ∀ i, ‖operatorRow (C i)‖ ≤ c) :
    ‖operatorRow (tupleOperatorProduct C)‖ ≤ c ^ n := by
…

Mentions: OAI.KadisonKastler.operatorRow, OAI.KadisonKastler.tupleOperatorProduct