OAI/Probability/RadialTransition/FamilyStep.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RadialTransition.prepend line 12
2. lemma OAI.RadialTransition.prepend_zero line 14
3. lemma OAI.RadialTransition.prepend_succ line 15
4. lemma OAI.RadialTransition.summable_prepend line 17
5. lemma OAI.RadialTransition.tsum_prepend line 21
6. lemma OAI.RadialTransition.prepend_nonneg line 25
7. lemma OAI.RadialTransition.prepend_range line 31
8. lemma OAI.RadialTransition.attractionProfile_prepend line 37
9. lemma OAI.RadialTransition.familyPotential_prepend line 46
10. lemma OAI.RadialTransition.familyCellMajorant_prepend line 53