OAI/Probability/FreeIsing/Estimates/InnovationCharacteristic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.InnovationCharacteristic.integrable_increment_sq_of_bounded_drift line 17
2. theorem OAI.Problem367.InnovationCharacteristic.norm_integral_test_increment_sq_error_le line 30
3. def OAI.Problem367.InnovationCharacteristic.driftMomentConstant line 64
4. theorem OAI.Problem367.InnovationCharacteristic.driftMomentConstant_nonneg line 67
5. theorem OAI.Problem367.InnovationCharacteristic.integral_increment_cube_le_common_constant line 73
6. theorem OAI.Problem367.InnovationCharacteristic.norm_integral_test_increment_sq_error_le_common_constant line 103
7. theorem OAI.Problem367.InnovationCharacteristic.integral_characteristic_eq_gaussian_of_bounded_drift line 135
8. theorem OAI.Problem367.InnovationCharacteristic.integral_characteristic_eq_gaussian_of_independent_enlargement line 163