OAI/Probability/RadialTransition/ParticleMeasure.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RadialTransition.ParticleState line 14
  2. instance OAI.RadialTransition.(instance at line 18) line 18
  3. instance OAI.RadialTransition.(instance at line 19) line 19
  4. def OAI.RadialTransition.particleCount line 21
  5. theorem OAI.RadialTransition.continuous_particleCount line 24
  6. theorem OAI.RadialTransition.measurable_particle_mk line 27
  7. theorem OAI.RadialTransition.measurable_particle_iff line 30
  8. def OAI.RadialTransition.particleBase line 43
  9. theorem OAI.RadialTransition.lintegral_particleBase line 47
  10. theorem OAI.RadialTransition.particleBase_univ line 58
  11. instance OAI.RadialTransition.particleBase_finite line 80
  12. def OAI.RadialTransition.particleVacuum line 86
  13. theorem OAI.RadialTransition.dirac_vacuum_le_particleBase line 88
  14. theorem OAI.RadialTransition.lintegral_exp_particleCount line 95
  15. theorem OAI.RadialTransition.integrable_exp_particleCount line 112