OAI/Analysis/KadisonKastler/PointedPowerOperators.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Local operators on the configuration Hilbert space

Finite matrix coefficients act on one configuration coordinate. The construction is a star homomorphism, so the local matrix-unit relations hold as actual bounded operator identities.

  1. def OAI.KadisonKastler.finiteLocalCoefficient line 24
  2. theorem OAI.KadisonKastler.finiteLocalCoefficient_mul line 27
  3. theorem OAI.KadisonKastler.finiteLocalCoefficient_star line 44
  4. def OAI.KadisonKastler.finiteLocalAmplificationValue line 55
  5. theorem OAI.KadisonKastler.finiteLocalAmplificationValue_apply line 63
  6. def OAI.KadisonKastler.finiteLocalAmplification line 70

    Source documentation

    Amplification of a finite-dimensional operator by an identity.

    def finiteLocalAmplification :
    (EuclideanSpace ℂ ι →L[ℂ] EuclideanSpace ℂ ι) →⋆ₐ[ℂ]
      (FiniteHilbert ι E →L[ℂ] FiniteHilbert ι E) where
…
  7. theorem OAI.KadisonKastler.finiteLocalAmplification_apply line 101
  8. def OAI.KadisonKastler.pointedPowerOperator line 110

    Source documentation

    Apply a four-dimensional operator at one site of the Hilbert product.

    def pointedPowerOperator (i : ℕ) :
    (EuclideanSpace ℂ (Fin 4) →L[ℂ] EuclideanSpace ℂ (Fin 4)) →⋆ₐ[ℂ]
      (PointedPowerHilbert →L[ℂ] PointedPowerHilbert) :=
…

    Mentions: OAI.KadisonKastler.PointedPowerHilbert

  9. theorem OAI.KadisonKastler.pointedPowerOperator_basis line 116
  10. theorem OAI.KadisonKastler.pointedPowerOperator_commute line 137

    Source documentation

    Operators on different sites commute, with no condition on their matrices.

    theorem pointedPowerOperator_commute {i j : ℕ} (hij : i ≠ j)
    (A B : EuclideanSpace ℂ (Fin 4) →L[ℂ] EuclideanSpace ℂ (Fin 4)) :
    Commute (pointedPowerOperator i A) (pointedPowerOperator j B) := by
…

    Mentions: OAI.KadisonKastler.pointedPowerOperator