OAI/Probability/RadialTransition/MultisetEnergy.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.multisetPairing line 19
  2. def OAI.RadialTransition.multisetDiagonal line 22
  3. def OAI.RadialTransition.multisetEnergy line 25
  4. lemma OAI.RadialTransition.multisetPairing_zero_left line 28
  5. lemma OAI.RadialTransition.multisetPairing_zero_right line 30
  6. lemma OAI.RadialTransition.multisetPairing_add_left line 32
  7. lemma OAI.RadialTransition.multisetPairing_add_right line 35
  8. lemma OAI.RadialTransition.multisetDiagonal_add line 38
  9. lemma OAI.RadialTransition.multisetDiagonal_zero line 41
  10. lemma OAI.RadialTransition.multisetPairing_symm line 43
  11. lemma OAI.RadialTransition.multisetEnergy_add line 52
  12. lemma OAI.RadialTransition.sum_map_configuration line 58
  13. lemma OAI.RadialTransition.multisetPairing_configuration line 64
  14. lemma OAI.RadialTransition.multisetDiagonal_configuration line 69
  15. lemma OAI.RadialTransition.multisetEnergy_particle line 73
  16. lemma OAI.RadialTransition.multisetPairing_fin_sum_left line 91
  17. lemma OAI.RadialTransition.multisetPairing_fin_sum_right line 99
  18. lemma OAI.RadialTransition.multisetDiagonal_fin_sum line 107
  19. lemma OAI.RadialTransition.multisetEnergy_sum line 115
  20. lemma OAI.RadialTransition.multisetEnergy_mappedMulti line 132
  21. lemma OAI.RadialTransition.continuous_multisetPairing_right line 155
  22. lemma OAI.RadialTransition.continuous_multisetEnergy_configuration line 164
  23. lemma OAI.RadialTransition.continuousConfiguration_boltzmann line 174
  24. def OAI.RadialTransition.radialPair line 187
  25. lemma OAI.RadialTransition.continuous_radialPair line 189
  26. lemma OAI.RadialTransition.radialPair_symm line 193
  27. lemma OAI.RadialTransition.pairWithin_radial line 196
  28. lemma OAI.RadialTransition.multisetEnergy_radial line 210
  29. lemma OAI.RadialTransition.measurable_particleBoltzmann line 214
  30. lemma OAI.RadialTransition.lintegral_grandOn line 221
  31. lemma OAI.RadialTransition.continuous_radialPair_comp line 240
  32. theorem OAI.RadialTransition.grandOn_cell_factorization line 247