OAI/Combinatorics/KMedian/Analysis/FiniteAverages.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.FiniteComparison.psi line 10
  2. def OAI.MetricKMedian.FiniteComparison.kZero line 12
  3. def OAI.MetricKMedian.FiniteComparison.kappa line 15
  4. theorem OAI.MetricKMedian.FiniteComparison.denominator_pos line 18
  5. theorem OAI.MetricKMedian.FiniteComparison.psi_nonneg line 22
  6. theorem OAI.MetricKMedian.FiniteComparison.psi_le_one line 26
  7. theorem OAI.MetricKMedian.FiniteComparison.psi_affine_majorant line 31
  8. theorem OAI.MetricKMedian.FiniteComparison.kZero_nonneg line 42
  9. theorem OAI.MetricKMedian.FiniteComparison.kappa_zero_le line 49
  10. theorem OAI.MetricKMedian.FiniteComparison.kappa_one_le line 72
  11. def OAI.MetricKMedian.FiniteComparison.average line 88
  12. theorem OAI.MetricKMedian.FiniteComparison.average_mono line 91
  13. theorem OAI.MetricKMedian.FiniteComparison.average_nonneg line 95
  14. theorem OAI.MetricKMedian.FiniteComparison.average_const line 99
  15. theorem OAI.MetricKMedian.FiniteComparison.average_add line 103
  16. theorem OAI.MetricKMedian.FiniteComparison.average_sub line 107
  17. theorem OAI.MetricKMedian.FiniteComparison.average_mul line 111
  18. theorem OAI.MetricKMedian.FiniteComparison.average_mul_right line 115
  19. def OAI.MetricKMedian.FiniteComparison.C line 119
  20. def OAI.MetricKMedian.FiniteComparison.k line 120
  21. def OAI.MetricKMedian.FiniteComparison.H line 121
  22. def OAI.MetricKMedian.FiniteComparison.d line 122
  23. def OAI.MetricKMedian.FiniteComparison.K line 124
  24. def OAI.MetricKMedian.FiniteComparison.L line 126
  25. def OAI.MetricKMedian.FiniteComparison.M line 128
  26. def OAI.MetricKMedian.FiniteComparison.G line 130
  27. def OAI.MetricKMedian.FiniteComparison.centered line 133
  28. theorem OAI.MetricKMedian.FiniteComparison.C_pos line 140
  29. theorem OAI.MetricKMedian.FiniteComparison.C_le_one line 143
  30. theorem OAI.MetricKMedian.FiniteComparison.centering_gap_nonneg line 146
  31. structure OAI.MetricKMedian.FiniteComparison.ScalarBounds line 155
  32. theorem OAI.MetricKMedian.FiniteComparison.centered_le_linear line 176
  33. theorem OAI.MetricKMedian.FiniteComparison.affine_hinge_nonpos line 191
  34. theorem OAI.MetricKMedian.FiniteComparison.average_exchange line 208
  35. theorem OAI.MetricKMedian.FiniteComparison.charge_cancellation line 220
  36. def OAI.MetricKMedian.FiniteComparison.rowValue line 247
  37. theorem OAI.MetricKMedian.FiniteComparison.taper_weighted_comparison line 254
  38. theorem OAI.MetricKMedian.FiniteComparison.row_as_average line 267
  39. theorem OAI.MetricKMedian.FiniteComparison.row_le_centered line 278
  40. theorem OAI.MetricKMedian.FiniteComparison.average_linear line 302
  41. theorem OAI.MetricKMedian.FiniteComparison.row_le_linear line 310
  42. theorem OAI.MetricKMedian.FiniteComparison.rate_comparison line 322
  43. theorem OAI.MetricKMedian.FiniteComparison.average_unit_bounds line 337