OAI/Analysis/KadisonKastler/PointedSiteBalance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The weighted trace identity at a matrix site

Product moments identify the two weights in the KMS balance equation. The identity is first proved in a finite block containing the site, then extended to the actual von Neumann closure by strong density.

  1. theorem OAI.KadisonKastler.weighted_productState_generated line 23
  2. theorem OAI.KadisonKastler.PointedMatrixSites.site_balance_blockEntry line 54
  3. theorem OAI.KadisonKastler.PointedMatrixSites.site_balance_finiteBlock line 82
  4. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatio_site_balance line 108

    Source documentation

    The weighted site identity holds against every operator in the product algebra.

    theorem twoRatio_site_balance (T : PointedMatrixSites M Ω twoRatioSiteParameter)
    (i : TwoRatioSite) (a b : Fin 2) (x : H →L[ℂ] H) (hx : x ∈ M) :
    (twoSiteWeight (twoRatioSiteParameter i) b : ℂ) *
        productVectorState Ω ((T.site i).entry a b * x) =
      (twoSiteWeight (twoRatioSiteParameter i) a : ℂ) *
        productVectorState Ω (x * (T.site i).entry a b) := by
…

    Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.twoRatioSiteParameter, OAI.KadisonKastler.TwoRatioSite, OAI.KadisonKastler.twoSiteWeight, OAI.KadisonKastler.productVectorState