OAI/Analysis/KadisonKastler/MultiplicationCorrectionTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.transportBilinear line 15
2. theorem OAI.KadisonKastler.transportBilinear_apply line 23
3. theorem OAI.KadisonKastler.transportBilinear_assoc line 28
4. theorem OAI.KadisonKastler.transportBilinear_star line 36
5. theorem OAI.KadisonKastler.bilinearProduct_transport_defect line 43
6. theorem OAI.KadisonKastler.starAlgEquiv_matrix_norm line 54
7. theorem OAI.KadisonKastler.transportBilinear_defect_bound line 59
8. theorem OAI.KadisonKastler.multiplication_correction_of_operator_model line 72

   Source documentation

   An operator-algebra model transfers the constructed correction, without any dependence on the multiplicity of the original representation.

   theorem multiplication_correction_of_operator_model
       {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H]
       (e : A ≃⋆ₐ[ℂ] (H →L[ℂ] H))
       (m : A →ₗ[ℂ] A →ₗ[ℂ] A)
       (hm : ∀ x y z, m (m x y) z = m x (m y z))
       (hms : ∀ x y, star (m x y) = m (star y) (star x))
       {q : ℝ} (hq : 0 ≤ q) (hq1 : q ≤ 1/11)
       (hb : HaagerupBound (m - LinearMap.mul ℂ A) q) :
       ∃ L : A ≃ₗ[ℂ] A, (∀ x y, L (m x y) = L x * L y) ∧
         (∀ x, L (star x) = star (L x)) ∧
         CompletelyBoundedBy (L.toLinearMap - LinearMap.id) (4 * q) := by
   …

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