OAI/Probability/SpanningForest/CharacteristicRemainder.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.Innovation.norm_exp_mul_I_remainder_le line 12
2. theorem OAI.Problem336.Innovation.norm_integral_exp_remainder_le line 54
3. theorem OAI.Problem336.Innovation.norm_condExp_exp_remainder_le line 98
4. theorem OAI.Problem336.Innovation.norm_sub_gaussian_char_le line 161
5. theorem OAI.Problem336.Innovation.conditional_characteristic_error line 196