OAI/Probability/SpanningForest/InnovationMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.InnovationMoments.abs_square_perturbation_le line 12
2. theorem OAI.Problem336.InnovationMoments.abs_cube_perturbation_le line 23
3. theorem OAI.Problem336.InnovationMoments.square_perturbation_le line 30
4. theorem OAI.Problem336.InnovationMoments.integrable_square_add_of_bounded line 39
5. theorem OAI.Problem336.InnovationMoments.integrable_abs_cube_add_of_bounded line 51
6. theorem OAI.Problem336.InnovationMoments.integral_square_perturbation_le line 66
7. theorem OAI.Problem336.InnovationMoments.integral_abs_cube_perturbation_le line 89