OAI/Combinatorics/KMedian/Geometry/MomentAnalysis.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Analytic.moment line 13
  2. theorem OAI.MetricKMedian.Analytic.moment_integrable line 15
  3. theorem OAI.MetricKMedian.Analytic.kernel_deriv line 20
  4. theorem OAI.MetricKMedian.Analytic.hasDerivAt_moment line 27
  5. theorem OAI.MetricKMedian.Analytic.moment_nonneg line 70
  6. theorem OAI.MetricKMedian.Analytic.moment_le_one line 75
  7. theorem OAI.MetricKMedian.Analytic.P_eq_moment line 84
  8. theorem OAI.MetricKMedian.Analytic.A_eq_moment line 86
  9. theorem OAI.MetricKMedian.Analytic.hasDerivAt_A line 92
  10. theorem OAI.MetricKMedian.Analytic.hasDerivAt_B line 100
  11. theorem OAI.MetricKMedian.Analytic.differential_identity line 106
  12. def OAI.MetricKMedian.Analytic.coefficient line 120
  13. theorem OAI.MetricKMedian.Analytic.coefficient_eq line 122
  14. theorem OAI.MetricKMedian.Analytic.coefficient_ge_one line 126
  15. theorem OAI.MetricKMedian.Analytic.coefficient_identity_drift line 132
  16. theorem OAI.MetricKMedian.Analytic.hasDerivAt_coefficient line 140