CutFactorization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact matrix factorizations of ordered cut sums

These identities turn the combinatorial splitting of a word into a row-matrix-column product. The identities apply to arbitrary prefix and suffix operators.

theorem OAI.KadisonKastler.operator_sandwich_entry line 30

Source documentation

Expand the single entry of an operator row-matrix-column product.

theorem operator_sandwich_entry {I J : Type*} [Fintype I] [Fintype J]
    (L : I → H →L[ℂ] H) (T : CStarMatrix I J (H →L[ℂ] H))
    (R : J → H →L[ℂ] H) :
    (operatorRow L * T * operatorColumn R) () () =
      ∑ i, ∑ j, L i * T i j * R j := by
…

Mentions: OAI.KadisonKastler.operatorRow, OAI.KadisonKastler.operatorColumn

theorem OAI.KadisonKastler.noPreservation_sum_eq_sandwich line 42
Source documentation
Prefixes have length p and suffixes length q; the adjacency matrix takes column length first, hence its parameters are q p.
```
theorem noPreservation_sum_eq_sandwich (W : Finset α) (p q : ℕ)
    (L : OrderedLabelTuple W p → H →L[ℂ] H)
    (R : OrderedLabelTuple W q → H →L[ℂ] H) :
    (∑ t : OrderedLabelTuple W (p + q), L (tupleInitial t) * R (tupleFinal t)) =
      (operatorRow L * orderedNoPreservationMatrix (H := H) W q p * operatorColumn R) () () := by
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.tupleInitial, OAI.KadisonKastler.tupleFinal, OAI.KadisonKastler.operatorRow, OAI.KadisonKastler.orderedNoPreservationMatrix, OAI.KadisonKastler.operatorColumn

def OAI.KadisonKastler.orderedMissingLabelMatrix line 60

Source documentation

The operator at the uniquely omitted label, with zero on intersecting pairs.

def orderedMissingLabelMatrix (W : Finset α) {p q : ℕ} (hW : W.card = p + 1 + q)
    (D : α → H →L[ℂ] H) :
    CStarMatrix (OrderedLabelTuple W p) (OrderedLabelTuple W q) (H →L[ℂ] H) :=
…

Mentions: OAI.KadisonKastler.OrderedLabelTuple

theorem OAI.KadisonKastler.orderedMissingLabelMatrix_apply line 68
theorem OAI.KadisonKastler.sum_subtype_extension line 75

theorem OAI.KadisonKastler.preservation_sum_eq_sandwich line 91

Source documentation

The exact preservation-cut factorization, before any norm estimate.

theorem preservation_sum_eq_sandwich (W : Finset α) (p q : ℕ)
    (hW : W.card = p + 1 + q)
    (L : OrderedLabelTuple W p → H →L[ℂ] H) (D : α → H →L[ℂ] H)
    (R : OrderedLabelTuple W q → H →L[ℂ] H) :
    (∑ t : OrderedLabelTuple W (p + 1 + q),
      L (tupleDropMiddle t).val.1 * D (tupleMiddle t) * R (tupleDropMiddle t).val.2) =
      (operatorRow L * orderedMissingLabelMatrix W hW D * operatorColumn R) () () := by
…

Mentions: OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.tupleDropMiddle, OAI.KadisonKastler.tupleMiddle, OAI.KadisonKastler.operatorRow, OAI.KadisonKastler.orderedMissingLabelMatrix, OAI.KadisonKastler.operatorColumn

theorem OAI.KadisonKastler.preservationSubsetMatrix_apply line 112

Source documentation

The two diagonal compressions act entry by entry.

theorem preservationSubsetMatrix_apply (W : Finset α) {p q : ℕ}
    (hW : W.card = p + q + 1) (e : α → H →L[ℂ] H) (P : H →L[ℂ] H) (d : ℝ)
    (a : WordSubset W q) (b : WordSubset W p) :
    preservationSubsetMatrix W hW e P d a b =
      P * ((if h : Disjoint a.val b.val then e (missingWordLabel W hW a b h) else 0) -
        (d⁻¹ : ℂ) • (if Disjoint a.val b.val then 1 else 0)) * P := by
…

Mentions: OAI.KadisonKastler.WordSubset, OAI.KadisonKastler.preservationSubsetMatrix, OAI.KadisonKastler.missingWordLabel

theorem OAI.KadisonKastler.orderedMissingLabelMatrix_eq_preservation line 128

Source documentation

The missing-label matrix equals the compressed preservation matrix. The identity itself holds for every compression operator.

theorem orderedMissingLabelMatrix_eq_preservation (W : Finset α) {p q : ℕ}
    (hW : W.card = p + 1 + q) (e : α → H →L[ℂ] H) (P : H →L[ℂ] H) (d : ℝ) :
    orderedMissingLabelMatrix W hW (fun a => P * (e a - (d⁻¹ : ℂ) • 1) * P) =
      orderedPreservationMatrix W (p := q) (q := p) (by omega) e P d := by
…

Mentions: OAI.KadisonKastler.orderedMissingLabelMatrix, OAI.KadisonKastler.orderedPreservationMatrix