OAI/Analysis/KadisonKastler/ConstructedFiniteSpatial.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.constructed_complete_closeness_of_finiteFactor_equiv line 35

   Source documentation

   The concrete paired factor gives the required complete bound.

   theorem constructed_complete_closeness_of_finiteFactor_equiv
       (hM : Generator.IsII1Factor M.toStarSubalgebra)
       (hN : Generator.IsII1Factor N.toStarSubalgebra)
       (θ : Algebra M ≃⋆ₐ[ℂ] Algebra N) {δ : ℝ} (hδ : 0 ≤ δ)
       (hclose : ∀ x : Algebra M, ‖x.val - (θ x).val‖ ≤ δ * ‖x‖) :
       CompletelyBoundedBy (M.toStarSubalgebra.subtype.toLinearMap -
         (N.toStarSubalgebra.subtype.comp θ.toStarAlgHom).toAlgHom.toLinearMap)
         (1000000 * δ) := by
   …

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

2. theorem OAI.KadisonKastler.constructed_finiteFactor_spatial_of_near_starEquiv line 50

   Source documentation

   A nearby finite-factor isomorphism is spatial, with no published amplification or commutant-distance assumption.

   theorem constructed_finiteFactor_spatial_of_near_starEquiv
       (hM : Generator.IsII1Factor M.toStarSubalgebra)
       (hN : Generator.IsII1Factor N.toStarSubalgebra)
       (θ : Algebra M ≃⋆ₐ[ℂ] Algebra N)
       {δ : ℝ} (hδ : 0 ≤ δ) (hsmall : δ < 1 / 4000000)
       (hclose : ∀ x : Algebra M,
         ‖x.val - (θ x).val‖ ≤ δ * ‖x‖) :
       ∃ u : unitary (H →L[ℂ] H), Conjugates u M N ∧
         ‖(u : H →L[ℂ] H) - 1‖ ≤ 4000000 * δ := by
   …

   Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.Conjugates