OAI/Probability/RadialTransition/FockIntegral.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.functional_integral_equiv line 23
2. lemma OAI.RadialTransition.functional_sector line 35
3. lemma OAI.RadialTransition.functional_sector_card line 65
4. def OAI.RadialTransition.fockCoeff line 90
5. lemma OAI.RadialTransition.fockCoeff_choose line 92
6. lemma OAI.RadialTransition.ennreal_subsets_card line 106
7. lemma OAI.RadialTransition.ennreal_tsum_triangle line 112
8. def OAI.RadialTransition.fockIntegral line 131
9. lemma OAI.RadialTransition.fockIntegral_add line 135
10. def OAI.RadialTransition.configurationMultiset line 162
11. def OAI.RadialTransition.particleMultiset line 164
12. lemma OAI.RadialTransition.configurationMultiset_equiv line 166
13. lemma OAI.RadialTransition.configurationMultiset_sum line 170
14. def OAI.RadialTransition.ContinuousConfiguration line 178
15. lemma OAI.RadialTransition.continuous_particleObservable line 182
16. lemma OAI.RadialTransition.continuous_particlePairObservable line 189
17. lemma OAI.RadialTransition.fockIntegral_eq_lintegral line 203
18. lemma OAI.RadialTransition.particleBase_add_observable line 209