OAI/Combinatorics/KMedian/Analysis/TaylorExpansion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Analytic.expApprox line 10
  2. def OAI.MetricKMedian.Analytic.pTaylor line 13
  3. def OAI.MetricKMedian.Analytic.aTaylor line 16
  4. def OAI.MetricKMedian.Analytic.taylorError line 19
  5. theorem OAI.MetricKMedian.Analytic.expApprox_error line 21
  6. theorem OAI.MetricKMedian.Analytic.expApprox_integrable line 29
  7. theorem OAI.MetricKMedian.Analytic.texpApprox_integrable line 35
  8. theorem OAI.MetricKMedian.Analytic.integral_expApprox line 41
  9. theorem OAI.MetricKMedian.Analytic.integral_texpApprox line 60
  10. theorem OAI.MetricKMedian.Analytic.P_taylor_error line 79
  11. theorem OAI.MetricKMedian.Analytic.A_taylor_error line 99