OAI/Analysis/KadisonKastler/OperatorCochainColumn.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.cochainColumn line 22
2. theorem OAI.KadisonKastler.cochainColumn_apply line 26
3. def OAI.KadisonKastler.cochainColumnEvaluation line 29
4. theorem OAI.KadisonKastler.cochainColumnEvaluation_apply line 34
5. def OAI.KadisonKastler.operatorCochainContraction line 38
6. theorem OAI.KadisonKastler.operatorCochainContraction_apply line 44
7. def OAI.KadisonKastler.cochainColumnMatrix line 50
8. theorem OAI.KadisonKastler.cochainColumnMatrix_apply line 56
9. theorem OAI.KadisonKastler.hilbertMatrix_cochainColumnMatrix line 61
10. theorem OAI.KadisonKastler.norm_cochainColumnMatrix_le line 73
11. theorem OAI.KadisonKastler.operatorCochainContraction_matrix_action line 90

    Source documentation

    A matrix of contracted cochain values is obtained by applying the bilinear amplification to one rank-one column.

    theorem operatorCochainContraction_matrix_action
        {f : (H →L[ℂ] H) →ₗ[ℂ] (H →L[ℂ] H) →ₗ[ℂ] (H →L[ℂ] H)} {c : ℝ}
        (hf : HaagerupBound f c) (hc : 0 ≤ c) (φ : H →L[ℂ] ℂ) (ξ : H)
        {p r q : ℕ} (j : Fin q) (X : CStarMatrix (Fin p) (Fin r) (H →L[ℂ] H))
        (y : Generator.FiniteHilbert (Fin r) H) :
        rectangularHilbertMatrix (CStarMatrix.mapₗ (operatorCochainContraction hf hc φ ξ).toLinearMap X) y =
          rectangularHilbertMatrix (bilinearProduct f X (cochainColumnMatrix φ j y))
            (Generator.tupleSingle j ξ) := by
    …

    Mentions: OAI.KadisonKastler.HaagerupBound, OAI.Generator.FiniteHilbert, OAI.KadisonKastler.rectangularHilbertMatrix, OAI.KadisonKastler.operatorCochainContraction, OAI.KadisonKastler.bilinearProduct, OAI.KadisonKastler.cochainColumnMatrix, OAI.Generator.tupleSingle

12. theorem OAI.KadisonKastler.operatorCochainContraction_complete_bound line 113

    Source documentation

    The rank-one contraction has its exact complete bound.

    theorem operatorCochainContraction_complete_bound
        {f : (H →L[ℂ] H) →ₗ[ℂ] (H →L[ℂ] H) →ₗ[ℂ] (H →L[ℂ] H)} {c : ℝ}
        (hf : HaagerupBound f c) (hc : 0 ≤ c) (φ : H →L[ℂ] ℂ) (ξ : H) :
        CompletelyBoundedBy (operatorCochainContraction hf hc φ ξ).toLinearMap
          (c * ‖φ‖ * ‖ξ‖) := by
    …

    Mentions: OAI.KadisonKastler.HaagerupBound, OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.operatorCochainContraction