OAI/Probability/Renewal/GaussianCore.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HoneycombLocal.norm_iteratedDeriv_charFun_le line 10
2. lemma OAI.HoneycombLocal.taylorWithinEval_eq_univ line 20
3. lemma OAI.HoneycombLocal.taylor_charFun_bound_nonneg line 31
4. lemma OAI.HoneycombLocal.taylor_charFun_bound line 52
5. lemma OAI.HoneycombLocal.norm_pow_difference line 67
6. lemma OAI.HoneycombLocal.exp_neg_error_le line 82
7. lemma OAI.HoneycombLocal.gaussian_power_error line 90
8. lemma OAI.HoneycombLocal.normalized_gaussian_power_error line 124