OAI/Analysis/KadisonKastler/OperatorCochainResidual.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.mul_cochainColumn line 17
2. theorem OAI.KadisonKastler.cochainColumnMatrix_product line 23
3. theorem OAI.KadisonKastler.rectangularHilbertMatrix_add line 35
4. theorem OAI.KadisonKastler.rectangularHilbertMatrix_sub line 42
5. theorem OAI.KadisonKastler.operatorCochainContraction_residual_identity line 50

   Source documentation

   Evaluating the differential on the last rank-one column is exactly the negative residual of the contracted cochain.

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

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

6. theorem OAI.KadisonKastler.operatorCochainContraction_residual_bound line 90

   Source documentation

   The contracted cochain leaves at most the exact quadratic differential bound. The estimate holds on every rectangular matrix pair.

   theorem operatorCochainContraction_residual_bound
       (m : (H →L[ℂ] H) →ₗ[ℂ] (H →L[ℂ] H) →ₗ[ℂ] (H →L[ℂ] H))
       (hm : ∀ x y z, m (m x y) z = m x (m y z)) {c : ℝ} (hc : 0 ≤ c)
       (hf : HaagerupBound (m - LinearMap.mul ℂ (H →L[ℂ] H)) c)
       (φ : H →L[ℂ] ℂ) (ξ : H) (hφ : φ ξ = 1) :
       HaagerupBound (m - LinearMap.mul ℂ (H →L[ℂ] H) -
         linearCoboundary (operatorCochainContraction hf hc φ ξ).toLinearMap)
         (2 * c ^ 2 * ‖φ‖ * ‖ξ‖) := by
   …

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