OAI/Analysis/OInfinity/FockConvergence.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Error bounds for the finite Fock approximation of O∞

  1. def OAI.WeakPureInfiniteness.fockGeneratorWeight line 33
  2. lemma OAI.WeakPureInfiniteness.fockGeneratorWeight_bounds line 36
  3. lemma OAI.WeakPureInfiniteness.oInfinityLevelDifference_sum_before line 53
  4. lemma OAI.WeakPureInfiniteness.weightedFockReturn_generator line 59
  5. def OAI.WeakPureInfiniteness.fockGeneratorError line 90
  6. lemma OAI.WeakPureInfiniteness.fockGeneratorError_nonneg line 94
  7. lemma OAI.WeakPureInfiniteness.fockGeneratorError_le_one line 101
  8. lemma OAI.WeakPureInfiniteness.fockGeneratorError_norm_le line 125
  9. lemma OAI.WeakPureInfiniteness.fockGenerator_normalization line 129
  10. def OAI.WeakPureInfiniteness.oInfinityFockApproximation line 153
  11. lemma OAI.WeakPureInfiniteness.oInfinityFockApproximation_one line 156
  12. lemma OAI.WeakPureInfiniteness.oInfinityFockApproximation_cp line 161
  13. lemma OAI.WeakPureInfiniteness.oInfinityFockApproximation_norm_le line 166
  14. lemma OAI.WeakPureInfiniteness.sub_eq_neg_of_sum line 171
  15. lemma OAI.WeakPureInfiniteness.oInfinityFockApproximation_generator_error line 176
  16. lemma OAI.WeakPureInfiniteness.oInfinityFockApproximation_generator_norm_le line 202
  17. lemma OAI.WeakPureInfiniteness.oInfinityFockApproximation_generator_tendsto line 219