OAI/Analysis/KadisonKastler/QuadraticMultiplicationCorrection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.quadratic_correction_half_bound line 14
2. theorem OAI.KadisonKastler.quadratic_multiplication_half_step line 23

   Source documentation

   A cochain with unit complete bound and quadratic coboundary error gives an invertible, star-preserving correction which halves the error.

   theorem quadratic_multiplication_half_step
       (m : A →ₗ[ℂ] A →ₗ[ℂ] A)
       (hm : ∀ x y z, m (m x y) z = m x (m y z))
       (hmstar : ∀ x y, star (m x y) = m (star y) (star x))
       {q : ℝ} (hq : 0 ≤ q) (hq1 : q ≤ 1 / 11)
       (hbound : HaagerupBound (m - LinearMap.mul ℂ A) q)
       (D : A →ₗ[ℂ] A) (hD : CompletelyBoundedBy D q)
       (hDstar : ∀ x, D (star x) = star (D x))
       (hres : HaagerupBound (m - LinearMap.mul ℂ A - linearCoboundary D) (2 * q ^ 2)) :
       ∃ L : A ≃ₗ[ℂ] A,
         L.toLinearMap = LinearMap.id + D ∧
         (∀ x, L (star x) = star (L x)) ∧
   …

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