FullOperatorMultiplicationCorrection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Constructed multiplication correction on the full operator algebra

The rank-one contraction provides the cochain required by the quantitative iteration. This proves the full-operator case; no claim about arbitrary von Neumann subalgebras is made here.

theorem OAI.KadisonKastler.fullOperator_quadraticCochainSolver line 24
Source documentation
The exact quadratic cochain estimate on all bounded operators.
```
theorem fullOperator_quadraticCochainSolver [Nontrivial H] :
    QuadraticCochainSolver (H →L[ℂ] H) := by
…
```
Mentions: OAI.KadisonKastler.QuadraticCochainSolver

theorem OAI.KadisonKastler.fullOperator_multiplication_correction line 48

Source documentation

An associative star product within1/11 of operator multiplication has a constructed star-preserving correcting equivalence, with complete bound4q.

theorem fullOperator_multiplication_correction [Nontrivial H]
    (m : (H →L[ℂ] H) →ₗ[ℂ] (H →L[ℂ] H) →ₗ[ℂ] (H →L[ℂ] H))
    (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 ℂ (H →L[ℂ] H)) q) :
    ∃ T : (H →L[ℂ] H) ≃ₗ[ℂ] (H →L[ℂ] H),
      (∀ x y, T (m x y) = T x * T y) ∧
      (∀ x, T (star x) = star (T x)) ∧
      CompletelyBoundedBy (T.toLinearMap - LinearMap.id) (4 * q) :=
…

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