OAI/Analysis/OInfinity/JordanWigner.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Finite Jordan–Wigner coordinates in a CAR corner

The occupation parities and their finite prefix products turn the given CAR modes into commuting two-level coordinates. All products below are finite; no representation or completion of an infinite CAR algebra is used.

  1. def OAI.WeakPureInfiniteness.carModeParity line 20

    Source documentation

    Twice the occupation projection is subtracted from the corner unit.

    def carModeParity (q a : E) : E := q - (star a * a + star a * a)
  2. lemma OAI.WeakPureInfiniteness.carModeParity_properties line 22
  3. lemma OAI.WeakPureInfiniteness.carOccupation_commute line 52
  4. lemma OAI.WeakPureInfiniteness.carModeParity_commute line 62
  5. def OAI.WeakPureInfiniteness.carParityPrefix line 69
  6. def OAI.WeakPureInfiniteness.carJordanWigner line 73
  7. lemma OAI.WeakPureInfiniteness.carFamily_square_zero line 83
  8. lemma OAI.WeakPureInfiniteness.carFamily_parity_properties line 88
  9. lemma OAI.WeakPureInfiniteness.carFamily_parity_commute line 99
  10. lemma OAI.WeakPureInfiniteness.carFamily_parities_commute line 105
  11. lemma OAI.WeakPureInfiniteness.carParityPrefix_support line 120
  12. lemma OAI.WeakPureInfiniteness.carParityPrefix_commute_parity line 136
  13. lemma OAI.WeakPureInfiniteness.carParityPrefix_properties line 147
  14. lemma OAI.WeakPureInfiniteness.carParityPrefix_commute line 170
  15. lemma OAI.WeakPureInfiniteness.carParityPrefix_commute_mode line 181
  16. lemma OAI.WeakPureInfiniteness.carParityPrefix_anticommute_mode line 190
  17. lemma OAI.WeakPureInfiniteness.carJordanWigner_support line 217
  18. lemma OAI.WeakPureInfiniteness.carJordanWigner_square_zero line 226
  19. lemma OAI.WeakPureInfiniteness.carJordanWigner_gram line 238
  20. lemma OAI.WeakPureInfiniteness.signedPrefix_commute line 267
  21. lemma OAI.WeakPureInfiniteness.carJordanWigner_commute_of_lt line 282
  22. lemma OAI.WeakPureInfiniteness.carJordanWigner_commute line 291
  23. lemma OAI.WeakPureInfiniteness.carJordanWigner_star line 299
  24. lemma OAI.WeakPureInfiniteness.carJordanWigner_star_commute_of_lt line 308
  25. lemma OAI.WeakPureInfiniteness.carJordanWigner_star_commute line 322
  26. def OAI.WeakPureInfiniteness.evenBlockFamily line 332

    Source documentation

    The concrete disjoint-block family underlying the commuting coordinates.

    def evenBlockFamily {n : ℕ} (r : Fin 2 × Fin n → E) (L : ℕ) (ζ : ℕ → ℂ) (i : ℕ) : E :=
…
  27. lemma OAI.WeakPureInfiniteness.evenBlockFamily_CAR line 335