UCP.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From a close UCP map to a star-algebra equivalence

The range argument and the multiplication-correction estimates give the isomorphism part of the manuscript's UCP criterion under PublishedMultiplicationCorrection. Complete positivity gives complete contractivity and star preservation.

theorem OAI.KadisonKastler.norm_le_of_completelyBoundedBy line 27
Source documentation
A complete bound implies the corresponding scalar bound.
```
theorem norm_le_of_completelyBoundedBy (F : A →ₗ[ℂ] B) {c : ℝ}
    (hF : CompletelyBoundedBy F c) (x : A) : ‖F x‖ ≤ c * ‖x‖ := by
…
```
Mentions: OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.bijective_ucp_of_reverse_gap line 56

Source documentation

A UCP map completely close to a faithful representation and with strict reverse unit-ball gap is bijective. Its normality is not needed.

theorem bijective_ucp_of_reverse_gap (M : VonNeumannAlgebra H)
    (φ : Algebra M →CP B) (hφ : φ 1 = 1)
    (ρ : Algebra M →⋆ₐ[ℂ] C) (ι : B →⋆ₐ[ℂ] C)
    (hρ : Function.Injective ρ) (hι : Function.Injective ι)
    {e g : ℝ} (he : 0 ≤ e) (he₁ : e < 1) (hge : g + e < 1)
    (hclose : CompletelyBoundedBy
      (ι.toAlgHom.toLinearMap.comp φ.toLinearMap - ρ.toAlgHom.toLinearMap) e)
    (hgap : ∀ y : B, ‖y‖ ≤ 1 → ∀ r : ℝ, g < r →
      ∃ x : Algebra M, ‖x‖ ≤ 1 ∧ ‖ι y - ρ x‖ < r) :
    Function.Bijective φ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.ucp_starEquiv_of_published line 77

Source documentation

The complete 32e isomorphism conclusion of the UCP criterion. The source is a concrete von Neumann algebra; the target may be any faithfully represented C*-algebra. Multiplication correction gives the star-algebra equivalence.

theorem ucp_starEquiv_of_published (M : VonNeumannAlgebra H)
    (hPublished : PublishedMultiplicationCorrection M)
    (φ : Algebra M →CP B) (hφ : φ 1 = 1)
    (ρ : Algebra M →⋆ₐ[ℂ] C) (ι : B →⋆ₐ[ℂ] C)
    (hρ : Function.Injective ρ) (hι : Function.Injective ι)
    {e g : ℝ} (he : 0 ≤ e) (he₁ : e < 1 / 1000) (hge : g + e < 1)
    (hclose : CompletelyBoundedBy
      (ι.toAlgHom.toLinearMap.comp φ.toLinearMap - ρ.toAlgHom.toLinearMap) e)
    (hgap : ∀ y : B, ‖y‖ ≤ 1 → ∀ r : ℝ, g < r →
      ∃ x : Algebra M, ‖x‖ ≤ 1 ∧ ‖ι y - ρ x‖ < r) :
    ∃ θ : Algebra M ≃⋆ₐ[ℂ] B,
      CompletelyBoundedBy
…

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