OAI/Probability/StrongRayleigh/ConditionalTaylor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.CharacteristicTaylor.abs_exp_neg_sub_one_add_le line 15
2. lemma OAI.Problem336AdditiveD139.CharacteristicTaylor.integrable_exp_I_mul line 31
3. theorem OAI.Problem336AdditiveD139.CharacteristicTaylor.condExp_quadratic_remainder_le line 39
4. theorem OAI.Problem336AdditiveD139.CharacteristicTaylor.conditional_characteristic_bound line 99