OAI/Probability/RadialTransition/GrandPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RadialTransition.grandOn line 12
2. theorem OAI.RadialTransition.partitionOn_stability_upper line 15
3. theorem OAI.RadialTransition.grandOn_term_upper line 35
4. theorem OAI.RadialTransition.grandOn_summable line 50
5. theorem OAI.RadialTransition.grandOn_bounds line 59
6. theorem OAI.RadialTransition.grandOn_union_lower line 74
7. theorem OAI.RadialTransition.grandOn_mono line 117
8. theorem OAI.RadialTransition.grandOn_translate line 125
9. theorem OAI.RadialTransition.grandOn_cube line 129