OAI/Probability/RadialTransition/PhysicalIteration.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RadialTransition.iterationMass line 10
2. def OAI.RadialTransition.iterationBudget line 11
3. lemma OAI.RadialTransition.iterationBudget_pos line 12
4. lemma OAI.RadialTransition.iterationMass_pos line 13
5. lemma OAI.RadialTransition.iterationMass_summable line 17
6. lemma OAI.RadialTransition.iterationMass_tsum line 19
7. lemma OAI.RadialTransition.iterationMass_le line 24
8. lemma OAI.RadialTransition.iterationMass_weight_summable line 26
9. lemma OAI.RadialTransition.iteration_admissible line 30
10. def OAI.RadialTransition.iterationQ line 35
11. def OAI.RadialTransition.iterationP line 38
12. lemma OAI.RadialTransition.iterationP_zero line 41
13. lemma OAI.RadialTransition.iterationP_succ line 44
14. lemma OAI.RadialTransition.iteration_kac line 46