OAI/Probability/RadialTransition/MeasurableFock.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.measurable_borel_sigma line 18
2. lemma OAI.RadialTransition.measurable_particle_prod line 32
3. def OAI.RadialTransition.MeasurableConfiguration line 57
4. lemma OAI.RadialTransition.measurable_particleObservable line 60
5. lemma OAI.RadialTransition.measurable_particlePairObservable line 66
6. lemma OAI.RadialTransition.fockIntegral_eq_lintegral_meas line 80
7. lemma OAI.RadialTransition.particleBase_add_observable_meas line 86
8. lemma OAI.RadialTransition.measurable_multiParticle_fixed line 152
9. lemma OAI.RadialTransition.measurable_configurationsInverse line 161
10. lemma OAI.RadialTransition.measurable_multiParticleObservable line 168
11. lemma OAI.RadialTransition.particleBase_zero_observable_meas line 187
12. lemma OAI.RadialTransition.particleBase_fin_sum_observable_meas line 199