OAI/Analysis/OInfinity/FockRangeProjection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Range projections in the finite Fock approximation

  1. lemma OAI.WeakPureInfiniteness.fockShift_adjoint_single_cons line 26
  2. lemma OAI.WeakPureInfiniteness.fockShift_adjoint_single_nil line 36
  3. lemma OAI.WeakPureInfiniteness.fockRangeProjection_single line 41
  4. lemma OAI.WeakPureInfiniteness.oInfinityFockCompression_rangeProjection line 52
  5. lemma OAI.WeakPureInfiniteness.fockRangeReturn_sum line 68
  6. lemma OAI.WeakPureInfiniteness.sum_fock_cons line 81
  7. lemma OAI.WeakPureInfiniteness.sum_finiteFock_rangePrefix line 87
  8. lemma OAI.WeakPureInfiniteness.unweightedFockReturn_rangeProjection line 107
  9. lemma OAI.WeakPureInfiniteness.weightedFockReturn_rangeProjection line 130
  10. lemma OAI.WeakPureInfiniteness.oInfinityFockApproximation_rangeProjection_succ line 162