OAI/Analysis/OInfinity/CPAP.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Completely positive finite-dimensional approximation of O∞

  1. def OAI.WeakPureInfiniteness.oInfinityApproximationSequence line 22
  2. lemma OAI.WeakPureInfiniteness.oInfinityApproximationSequence_one line 25
  3. lemma OAI.WeakPureInfiniteness.oInfinityApproximationSequence_cp line 28
  4. lemma OAI.WeakPureInfiniteness.oInfinityApproximationSequence_norm_le line 31
  5. lemma OAI.WeakPureInfiniteness.oInfinityApproximationSequence_generator_tendsto line 34
  6. lemma OAI.WeakPureInfiniteness.oInfinityApproximationSequence_rangeProjection_tendsto line 46
  7. lemma OAI.WeakPureInfiniteness.oInfinityApproximationSequence_word_tendsto line 66
  8. lemma OAI.WeakPureInfiniteness.oInfinityApproximationSequence_polynomial_tendsto line 93
  9. lemma OAI.WeakPureInfiniteness.oInfinityApproximationSequence_tendsto line 101
  10. abbrev OAI.WeakPureInfiniteness.oInfinityApproximationDimension line 124
  11. def OAI.WeakPureInfiniteness.oInfinityApproximationReindex line 127
  12. def OAI.WeakPureInfiniteness.oInfinityCPAPCompression line 133
  13. def OAI.WeakPureInfiniteness.oInfinityCPAPReturn line 140
  14. lemma OAI.WeakPureInfiniteness.oInfinityCPAPCompression_cp line 147
  15. lemma OAI.WeakPureInfiniteness.oInfinityCPAPReturn_cp line 153
  16. lemma OAI.WeakPureInfiniteness.oInfinityCPAPCompression_one line 159
  17. lemma OAI.WeakPureInfiniteness.oInfinityCPAPReturn_one line 163
  18. lemma OAI.WeakPureInfiniteness.oInfinityCPAP_comp line 167
  19. theorem OAI.WeakPureInfiniteness.oInfinity_nuclear line 176