OAI/Analysis/OInfinity/FockShift.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The finite Fock compression on a canonical generator

  1. lemma OAI.WeakPureInfiniteness.finiteFockWord_length line 12
  2. def OAI.WeakPureInfiniteness.finiteFockCons line 15
  3. lemma OAI.WeakPureInfiniteness.finiteFockWord_cons line 19
  4. lemma OAI.WeakPureInfiniteness.finiteFockAlgebraWord_cons line 24
  5. lemma OAI.WeakPureInfiniteness.oInfinityFockCompression_generator line 30
  6. lemma OAI.WeakPureInfiniteness.sum_finiteFock_prefix line 40
  7. lemma OAI.WeakPureInfiniteness.sum_finiteFock_prefix_boundary line 51
  8. lemma OAI.WeakPureInfiniteness.unweightedFockReturn_generator_sum line 62
  9. lemma OAI.WeakPureInfiniteness.unweightedFockReturn_generator line 76
  10. lemma OAI.WeakPureInfiniteness.weightedFockCoefficient_prefix line 97
  11. lemma OAI.WeakPureInfiniteness.weightedFockReturn_generator_sum line 120