OAI/Combinatorics/KMedian/Analysis/Coefficients.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.MainObligation line 9
  2. def OAI.MetricKMedian.Analytic.A line 18
  3. def OAI.MetricKMedian.Analytic.P line 21
  4. def OAI.MetricKMedian.Analytic.B line 24
  5. def OAI.MetricKMedian.Analytic.m line 26
  6. theorem OAI.MetricKMedian.Analytic.exp_integrable line 28
  7. theorem OAI.MetricKMedian.Analytic.texp_integrable line 33
  8. theorem OAI.MetricKMedian.Analytic.exp_derivative_integral line 38
  9. theorem OAI.MetricKMedian.Analytic.texp_derivative_integral line 50
  10. theorem OAI.MetricKMedian.Analytic.A_eq line 68
  11. theorem OAI.MetricKMedian.Analytic.coefficient_identity line 73
  12. theorem OAI.MetricKMedian.Analytic.drift_identity line 80
  13. theorem OAI.MetricKMedian.Analytic.A_zero line 86
  14. theorem OAI.MetricKMedian.Analytic.P_zero line 88
  15. theorem OAI.MetricKMedian.Analytic.A_one line 92
  16. theorem OAI.MetricKMedian.Analytic.P_nonneg line 101
  17. theorem OAI.MetricKMedian.Analytic.P_antitone line 106
  18. theorem OAI.MetricKMedian.Analytic.P_le_half line 114
  19. theorem OAI.MetricKMedian.Analytic.exp_neg_half_le_P line 117
  20. theorem OAI.MetricKMedian.Analytic.P_pos line 131
  21. theorem OAI.MetricKMedian.Analytic.one_le_A line 134
  22. theorem OAI.MetricKMedian.Analytic.A_le_one_add line 144
  23. theorem OAI.MetricKMedian.Analytic.A_le_two line 162
  24. theorem OAI.MetricKMedian.Analytic.m_nonneg line 165