OAI/Analysis/KadisonKastler/PairedAmplification.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.paired_switch_commutator line 25

   Source documentation

   The switch commutator records exactly the difference of the pair.

   theorem paired_switch_commutator (ρ θ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (x : A) :
       innerDerivation (blockFlip (A := H →L[ℂ] H) :
   …

   Mentions: OAI.KadisonKastler.innerDerivation, OAI.KadisonKastler.blockFlip

2. theorem OAI.KadisonKastler.paired_switch_commutator_norm line 31
3. theorem OAI.KadisonKastler.paired_switch_isSelfAdjoint line 38
4. theorem OAI.KadisonKastler.complete_closeness_of_paired_factor line 67

   Source documentation

   Once the paired representation is identified with a concrete II₁ factor, the uniform amplification theorem upgrades its scalar closeness to complete closeness. The identification is kept explicit for use in the original representation at the end of the finite-factor argument.

   theorem complete_closeness_of_paired_factor
       (hpub : PublishedTracialUltrapower.{u})
       (hmat : PublishedFiniteMatrixUltraproduct)
       (hind : PublishedPopaFiniteBaseIndependence.{u})
       (hP : Generator.IsII1Factor P.toStarSubalgebra)
       (hCyclic : PublishedCyclicSimilarity.{u, u} (A := Algebra P))
   …

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