PointedPowerMoments.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Independent-site vacuum moments in the countable product

The vacuum rank-one projection at one site commutes with all other sites. Its corner is the local vector state, giving product moments.

def OAI.KadisonKastler.pointedLocalVacuumProjection line 18
theorem OAI.KadisonKastler.pointedLocalVacuumProjection_apply line 21
theorem OAI.KadisonKastler.pointedLocalVacuumProjection_star line 25
theorem OAI.KadisonKastler.pointedLocalVacuumProjection_corner line 30
theorem OAI.KadisonKastler.pointedPowerVacuumProjection_fixes line 38
theorem OAI.KadisonKastler.pointedPowerVacuumProjection_star line 48
theorem OAI.KadisonKastler.vacuum_moment_split line 53

theorem OAI.KadisonKastler.pointedPower_product_moment line 83

Source documentation

The vacuum factors on every finite family of distinct sites.

theorem pointedPower_product_moment
    (A : ℕ → PointedLocalHilbert →L[ℂ] PointedLocalHilbert)
    (l : List ℕ) (hl : l.Nodup) :
    inner ℂ pointedPowerVacuum
      (((l.map fun i => pointedPowerOperator i (A i)).prod) pointedPowerVacuum) =
      (l.map fun i => inner ℂ pointedLocalVacuum (A i pointedLocalVacuum)).prod := by
…

Mentions: OAI.KadisonKastler.PointedLocalHilbert, OAI.KadisonKastler.pointedPowerVacuum, OAI.KadisonKastler.pointedPowerOperator, OAI.KadisonKastler.pointedLocalVacuum

theorem OAI.KadisonKastler.pointedPower_moments line 108

Source documentation

The configuration representation has exactly the prescribed matrix-state moments.

theorem pointedPower_moments {ν : ℝ} (d : PointedLocalMatrixData ν)
    (l : List ℕ) (hl : l.Nodup) (r c : ℕ → Fin 2) :
    inner ℂ pointedPowerVacuum
      (((l.map fun i => (pointedPowerSite d.left i).entry (r i) (c i)).prod)
        pointedPowerVacuum) =
      (l.map fun i => if r i = c i then (twoSiteWeight ν (r i) : ℂ) else 0).prod := by
…

Mentions: OAI.KadisonKastler.PointedLocalMatrixData, OAI.KadisonKastler.pointedPowerVacuum, OAI.KadisonKastler.pointedPowerSite, OAI.KadisonKastler.twoSiteWeight

theorem OAI.KadisonKastler.pointedPowerSite_commuting line 117