OAI/MathematicalPhysics/Heisenberg/StateCompactness.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Heisenberg.quasiLocalClosed line 13
  2. theorem OAI.Heisenberg.countable_monoidClosure line 16
  3. instance OAI.Heisenberg.quasiLocalSeparable line 30
  4. theorem OAI.Heisenberg.positive_norm_bound line 53
  5. theorem OAI.Heisenberg.state_norm_bound line 84
  6. theorem OAI.Heisenberg.bounded_functionals_subsequence line 91
  7. theorem OAI.Heisenberg.state_subsequence line 107
  8. def OAI.Heisenberg.operatorInclusion line 130
  9. def OAI.Heisenberg.vectorFunctional line 133
  10. theorem OAI.Heisenberg.vectorFunctional_apply line 137
  11. def OAI.Heisenberg.vectorState line 140
  12. def OAI.Heisenberg.configVector line 154
  13. theorem OAI.Heisenberg.norm_configVector line 157
  14. theorem OAI.Heisenberg.vectorFunctional_configVector line 161
  15. abbrev OAI.Heisenberg.FiniteConfiguration line 166
  16. def OAI.Heisenberg.extendConfig line 168
  17. theorem OAI.Heisenberg.extendConfig_apply line 173
  18. def OAI.Heisenberg.finiteTraceFunctional line 178
  19. theorem OAI.Heisenberg.finiteTraceFunctional_apply line 182
  20. def OAI.Heisenberg.finiteTraceState line 190
  21. theorem OAI.Heisenberg.configVector_apply line 221
  22. theorem OAI.Heisenberg.matrixUnit_configVector line 225
  23. def OAI.Heisenberg.finiteConfigPerm line 256
  24. theorem OAI.Heisenberg.extendConfig_perm line 263
  25. theorem OAI.Heisenberg.finiteTraceFunctional_cyclic_unit line 277
  26. theorem OAI.Heisenberg.cyclic_adjoin line 302
  27. theorem OAI.Heisenberg.cyclic_of_cyclic_units line 332
  28. theorem OAI.Heisenberg.exists_tracial_state line 346
  29. theorem OAI.Heisenberg.positive_norm_le_four_one line 358
  30. def OAI.Heisenberg.sandwichFunctional line 387
  31. theorem OAI.Heisenberg.sandwichFunctional_apply line 390
  32. theorem OAI.Heisenberg.sandwichFunctional_positive line 393
  33. theorem OAI.Heisenberg.sandwich_one_pos line 398
  34. def OAI.Heisenberg.sandwichState line 426
  35. def OAI.Heisenberg.gibbsDensity line 451
  36. def OAI.Heisenberg.gibbsHalf line 454
  37. lemma OAI.Heisenberg.star_gibbsHalf line 457
  38. lemma OAI.Heisenberg.gibbsHalf_sq line 462
  39. def OAI.Heisenberg.gibbsState line 470
  40. theorem OAI.Heisenberg.gibbs_normalization_pos line 473
  41. theorem OAI.Heisenberg.gibbsState_apply line 484
  42. theorem OAI.Heisenberg.exists_gibbs_states line 496