OAI/Probability/Ballisticity/Estimates/DifferentiableExp.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.differentiable_of_exp_eq line 20
2. lemma OAI.DirectionalTransience.exists_entire_log line 38
3. lemma OAI.DirectionalTransience.entire_norm_quadratic_bound line 51
4. lemma OAI.DirectionalTransience.entire_third_deriv_zero line 74
5. theorem OAI.DirectionalTransience.entire_log_quadratic line 97
6. theorem OAI.DirectionalTransience.entire_gaussian_factor line 131