OAI/Probability/RadialTransition/PairEnsembles.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.measurable_pairWithin line 20
2. lemma OAI.RadialTransition.measurable_pairBetween line 37
3. lemma OAI.RadialTransition.measurable_pairCellEnergy line 54
4. lemma OAI.RadialTransition.pairCellEnergy_no_cross line 73
5. lemma OAI.RadialTransition.boltzmannPartition_no_cross line 83
6. def OAI.RadialTransition.pairGrand line 98
7. lemma OAI.RadialTransition.pairGrand_eq_cell line 101
8. lemma OAI.RadialTransition.pairGrand_radial line 134