OAI/Probability/RadialTransition/CellMoments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.cell_young line 16
2. theorem OAI.RadialTransition.one_cell_exponential_moment line 21
3. def OAI.RadialTransition.cellN line 73
4. theorem OAI.RadialTransition.cellN_nonneg line 77
5. theorem OAI.RadialTransition.measurable_cellN line 81
6. theorem OAI.RadialTransition.integrable_exp_cell_total line 85
7. theorem OAI.RadialTransition.cell_partition_pos line 94
8. theorem OAI.RadialTransition.weighted_square_le line 110
9. theorem OAI.RadialTransition.integrable_cell_numerator line 118
10. theorem OAI.RadialTransition.uniform_cell_exponential_moment line 130