OAI/Analysis/OInfinity/FockCompression.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Finite Fock-space compression of the canonical O∞ model

  1. abbrev OAI.WeakPureInfiniteness.FiniteFockIndex line 13
  2. def OAI.WeakPureInfiniteness.finiteFockWord line 15
  3. lemma OAI.WeakPureInfiniteness.finiteFockWord_injective line 18
  4. def OAI.WeakPureInfiniteness.finiteFockVector line 34
  5. lemma OAI.WeakPureInfiniteness.finiteFockVector_orthonormal line 37
  6. def OAI.WeakPureInfiniteness.finiteFockLinear line 48
  7. lemma OAI.WeakPureInfiniteness.finiteFockLinear_basis line 54
  8. def OAI.WeakPureInfiniteness.finiteFockIsometry line 60
  9. def OAI.WeakPureInfiniteness.scalarMatrixOperatorEquiv line 70
  10. lemma OAI.WeakPureInfiniteness.scalarMatrixOperatorEquiv_basis line 74
  11. lemma OAI.WeakPureInfiniteness.scalarMatrixOperatorEquiv_symm_apply line 81
  12. def OAI.WeakPureInfiniteness.fockOperatorRepresentation line 89
  13. def OAI.WeakPureInfiniteness.oInfinityFockOperatorCompression line 92
  14. def OAI.WeakPureInfiniteness.oInfinityFockCompression line 98
  15. lemma OAI.WeakPureInfiniteness.oInfinityFockOperatorCompression_cp line 107
  16. lemma OAI.WeakPureInfiniteness.oInfinityFockOperatorCompression_norm_le line 111
  17. lemma OAI.WeakPureInfiniteness.oInfinityFockCompression_cp line 118
  18. lemma OAI.WeakPureInfiniteness.oInfinityFockCompression_norm_le line 125
  19. lemma OAI.WeakPureInfiniteness.finiteFockIsometry_basis line 140
  20. lemma OAI.WeakPureInfiniteness.oInfinityFockCompression_apply line 144
  21. lemma OAI.WeakPureInfiniteness.oInfinityFockCompression_one line 160