OAI/Probability/RadialTransition/MultiConvolution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.particleBase_emptyWeight line 16
2. def OAI.RadialTransition.finClusterProduct line 25
3. lemma OAI.RadialTransition.measurable_finClusterProduct line 30
4. lemma OAI.RadialTransition.finClusterProduct_ge line 37
5. lemma OAI.RadialTransition.particleBase_finClusterProduct line 46
6. def OAI.RadialTransition.indexedClusterProduct line 58
7. lemma OAI.RadialTransition.measurable_indexedClusterProduct line 62
8. lemma OAI.RadialTransition.indexedClusterProduct_ge line 67
9. lemma OAI.RadialTransition.particleBase_indexedClusterProduct line 74