ConcreteUCP.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The UCP criterion for concrete von Neumann algebras

The ordinary Kadison--Kastler gap supplies precisely the reverse unit-ball approximation used in the UCP range argument.

abbrev OAI.KadisonKastler.algebraInclusion line 33
Source documentation
The faithful inclusion of a concrete von Neumann algebra into its ambient bounded operators.
```
abbrev algebraInclusion (M : VonNeumannAlgebra H) :
    Algebra M →⋆ₐ[ℂ] (H →L[ℂ] H) := M.toStarSubalgebra.subtype
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.reverse_gap_of_kkDistance_lt line 36

theorem OAI.KadisonKastler.conjugates_of_starEquiv line 49

Source documentation

An intertwining star-algebra equivalence gives equality of the concrete algebras after unitary conjugation.

theorem conjugates_of_starEquiv {M N : VonNeumannAlgebra H}
    (θ : Algebra M ≃⋆ₐ[ℂ] Algebra N) (u : unitary (H →L[ℂ] H))
    (hθ : ∀ x : Algebra M,
      (u : H →L[ℂ] H) * algebraInclusion M x * star (u : H →L[ℂ] H) =
        algebraInclusion N (θ x)) :
    Conjugates u M N := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.algebraInclusion, OAI.KadisonKastler.Conjugates

theorem OAI.KadisonKastler.concrete_ucp_starEquiv_of_published line 69

Source documentation

The concrete-algebra isomorphism part of the UCP criterion, with the ordinary metric used only for the reverse gap.

theorem concrete_ucp_starEquiv_of_published {M N : VonNeumannAlgebra H}
    (hPublished : PublishedMultiplicationCorrection M)
    (φ : Algebra M →CP Algebra N) (hφ : φ 1 = 1)
    {e g : ℝ} (he : 0 ≤ e) (he₁ : e < 1 / 1000) (hge : g + e < 1)
    (hclose : CompletelyBoundedBy
      ((algebraInclusion N).toAlgHom.toLinearMap.comp φ.toLinearMap -
        (algebraInclusion M).toAlgHom.toLinearMap) e)
    (hgap : kkDistance M N < g) :
    ∃ θ : Algebra M ≃⋆ₐ[ℂ] Algebra N,
      CompletelyBoundedBy
        ((algebraInclusion N).toAlgHom.toLinearMap.comp θ.toAlgEquiv.toLinearMap -
          (algebraInclusion M).toAlgHom.toLinearMap) (32 * e) := by
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.algebraInclusion, OAI.KadisonKastler.kkDistance

theorem OAI.KadisonKastler.concrete_ucp_unitary_of_published line 88

Source documentation

The unitary-conjugacy conclusion of the UCP criterion for concrete algebras. Both published inputs are explicit, while positivity, surjectivity, correction estimates, and polar implementation are proved.

theorem concrete_ucp_unitary_of_published {M N : VonNeumannAlgebra H}
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (φ : Algebra M →CP Algebra N) (hφ : φ 1 = 1)
    {e g : ℝ} (he : 0 ≤ e) (he₁ : e < 1 / 1000) (hge : g + e < 1)
    (hclose : CompletelyBoundedBy
      ((algebraInclusion N).toAlgHom.toLinearMap.comp φ.toLinearMap -
        (algebraInclusion M).toAlgHom.toLinearMap) e)
    (hgap : kkDistance M N < g) :
    ∃ u : unitary (H →L[ℂ] H),
      Conjugates u M N ∧ ‖(u : H →L[ℂ] H) - 1‖ ≤ 128 * e := by
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.algebraInclusion, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Conjugates