OAI/Probability/GaussianPropeller/Taylor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianPropeller.Taylor.E line 28
  2. def OAI.GaussianPropeller.Taylor.J line 30
  3. lemma OAI.GaussianPropeller.Taylor.E_zero line 33
  4. lemma OAI.GaussianPropeller.Taylor.exp_remainder line 41
  5. lemma OAI.GaussianPropeller.Taylor.exp_le_E_even line 59
  6. lemma OAI.GaussianPropeller.Taylor.E_odd_le_exp line 71
  7. lemma OAI.GaussianPropeller.Taylor.hasDerivAt_J line 80
  8. lemma OAI.GaussianPropeller.Taylor.J_zero line 95
  9. lemma OAI.GaussianPropeller.Taylor.integral_E line 97
  10. lemma OAI.GaussianPropeller.Taylor.integral_exp_bounds line 105