OAI/Analysis/KadisonKastler/PointedPowerConfigurations.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Configuration coordinates for a pointed countable Hilbert product

A configuration records the finitely many sites outside the reference vector. Splitting off one site gives a finite Hilbert sum of identical tail spaces, with an explicit action on every orthonormal basis vector.

  1. abbrev OAI.KadisonKastler.PointedPowerConfiguration line 23
  2. abbrev OAI.KadisonKastler.PointedPowerHilbert line 24
  3. def OAI.KadisonKastler.pointedPowerBasis line 26
  4. def OAI.KadisonKastler.pointedPowerVacuum line 29
  5. theorem OAI.KadisonKastler.norm_pointedPowerBasis line 31
  6. theorem OAI.KadisonKastler.norm_pointedPowerVacuum line 35
  7. def OAI.KadisonKastler.pointedPowerHilbertBasis line 38
  8. theorem OAI.KadisonKastler.pointedPowerHilbertBasis_apply line 41
  9. instance OAI.KadisonKastler.(instance at line 45) line 45
  10. instance OAI.KadisonKastler.(instance at line 53) line 53
  11. abbrev OAI.KadisonKastler.PointedPowerTail line 66
  12. abbrev OAI.KadisonKastler.PointedPowerTailHilbert line 67
  13. def OAI.KadisonKastler.pointedPowerSplit line 70

    Source documentation

    A configuration is its label at one site and the vacuum-filled tail.

    def pointedPowerSplit (i : ℕ) :
    PointedPowerConfiguration ≃ Fin 4 × PointedPowerTail i where
…

    Mentions: OAI.KadisonKastler.PointedPowerConfiguration, OAI.KadisonKastler.PointedPowerTail

  14. theorem OAI.KadisonKastler.pointedPowerSplit_fst line 90
  15. theorem OAI.KadisonKastler.pointedPowerSplit_symm line 93
  16. def OAI.KadisonKastler.finiteL2BasisVector line 100
  17. theorem OAI.KadisonKastler.finiteL2BasisVector_orthonormal line 103
  18. theorem OAI.KadisonKastler.finiteL2BasisVector_total line 114
  19. def OAI.KadisonKastler.finiteL2Basis line 138

    Source documentation

    The usual basis of the finite sum of scalar l² spaces.

    def finiteL2Basis : HilbertBasis (ι × κ) ℂ (FiniteHilbert ι ℓ²(κ, ℂ)) :=
…
  20. theorem OAI.KadisonKastler.finiteL2Basis_apply line 141
  21. def OAI.KadisonKastler.pointedPowerSplitBasis line 147
  22. theorem OAI.KadisonKastler.pointedPowerSplitBasis_apply line 162
  23. def OAI.KadisonKastler.pointedPowerFibreEquiv line 168

    Source documentation

    Splitting off one site is a genuine Hilbert-space equivalence.

    def pointedPowerFibreEquiv (i : ℕ) :
    PointedPowerHilbert ≃ₗᵢ[ℂ] FiniteHilbert (Fin 4) (PointedPowerTailHilbert i) :=
…

    Mentions: OAI.KadisonKastler.PointedPowerHilbert, OAI.KadisonKastler.PointedPowerTailHilbert

  24. theorem OAI.KadisonKastler.pointedPowerFibreEquiv_basis line 172