OAI/Analysis/OInfinity/NuclearModel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite-level identities for the nuclear approximation of O∞

The shift by a finite set of canonical isometries and its level projections give the telescoping weights for finite Fock-space compressions.

  1. lemma OAI.WeakPureInfiniteness.finiteCuntz_conjugate_mul line 24
  2. def OAI.WeakPureInfiniteness.oInfinityFiniteShift line 46
  3. def OAI.WeakPureInfiniteness.oInfinityLevel line 64
  4. lemma OAI.WeakPureInfiniteness.oInfinityLevel_zero line 68
  5. lemma OAI.WeakPureInfiniteness.oInfinityLevel_succ line 70
  6. lemma OAI.WeakPureInfiniteness.oInfinityLevel_nonneg line 73
  7. lemma OAI.WeakPureInfiniteness.oInfinityLevel_idempotent line 78
  8. lemma OAI.WeakPureInfiniteness.oInfinityLevel_antitone line 85
  9. def OAI.WeakPureInfiniteness.oInfinityLevelDifference line 98
  10. lemma OAI.WeakPureInfiniteness.oInfinityLevelDifference_nonneg line 101
  11. lemma OAI.WeakPureInfiniteness.oInfinityLevelDifference_sum line 105
  12. lemma OAI.WeakPureInfiniteness.oInfinityLevel_weighted_sum line 115