OAI/Analysis/KadisonKastler/TwoRatioProductConstruction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The two-ratio product

The finite and remote matrix stages are concrete products. The two off-diagonal modular eigenvalues follow from their finite product moments and the KMS characterization of the supplied modular resolution.

  1. def OAI.KadisonKastler.PointedMatrixProduct.toTwoRatioProductModel line 19
  2. def OAI.KadisonKastler.concreteTwoRatioProductModel line 38
  3. theorem OAI.KadisonKastler.publishedTwoRatioProduct line 42

    Source documentation

    Blackadar, III.3.1.1--3 and III.4.4.7--9, in exactly the application scope.

    theorem publishedTwoRatioProduct : PublishedTwoRatioProduct.{u} :=
…