OAI/Probability/StrongRayleigh/CharacteristicTaylor.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.CharacteristicTaylor.norm_sub_zero_le_of_deriv_bound line 14
2. theorem OAI.Problem336AdditiveD139.CharacteristicTaylor.norm_exp_I_mul_sub_one_sub_linear line 37
3. theorem OAI.Problem336AdditiveD139.CharacteristicTaylor.norm_exp_I_mul_sub_quadratic line 56