PublishedCorrection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The published multiplication-correction input

PublishedMultiplicationCorrection is the application of Ricard--Roydor, A non-commutative Amir--Cambern theorem for von Neumann algebras and nuclear C-algebras*, J. Funct. Anal. 267 (2014), Proposition 3.2 (arXiv:1108.1970v2), to associative, involution-compatible products on a concrete von Neumann algebra. It is an explicit hypothesis, not an axiom.

The downstream theorem constructs the corrected star-algebra equivalence and proves the 32e complete bound. Surjectivity of the original map and spatial implementation are treated separately.

def OAI.KadisonKastler.PublishedMultiplicationCorrection line 37
Source documentation
The precise published input used for correction. No normality is required of the perturbed multiplication or of the correcting map.
```
def PublishedMultiplicationCorrection (M : VonNeumannAlgebra H) : Prop :=
…
```
theorem OAI.KadisonKastler.linear_correction_of_published line 52

theorem OAI.KadisonKastler.corrected_equivalence_of_published line 69

Source documentation

The algebraic-isomorphism part of the UCP criterion, conditional only on the published correction theorem. Complete contractivity and the linear equivalence are explicit here; later steps supply them from positivity and the reverse unit-ball gap.

theorem corrected_equivalence_of_published (M : VonNeumannAlgebra H)
    (hPublished : PublishedMultiplicationCorrection M)
    (F : Algebra M ≃ₗ[ℂ] B) (ρ : Algebra M →ₐ[ℂ] C) (ι : B →ₐ[ℂ] C)
    (hFstar : ∀ x, F (star x) = star (F x))
    {e : ℝ} (he : 0 ≤ e) (he₁ : e < 1 / 1000)
    (hρ : CompletelyIsometric ρ.toLinearMap)
    (hι : CompletelyIsometric ι.toLinearMap)
    (hF : CompletelyBoundedBy F.toLinearMap 1)
    (hclose : CompletelyBoundedBy (ι.toLinearMap.comp F.toLinearMap - ρ.toLinearMap) e) :
    ∃ θ : Algebra M ≃⋆ₐ[ℂ] B,
      CompletelyBoundedBy (ι.toLinearMap.comp θ.toAlgEquiv.toLinearMap - ρ.toLinearMap)
        (32 * e) := by
…

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