OAI/Combinatorics/KMedian/Analysis/FiniteComparison.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.FiniteComparison.actualB line 15
  2. theorem OAI.MetricKMedian.FiniteComparison.scalarC line 18
  3. theorem OAI.MetricKMedian.FiniteComparison.scalarD line 20
  4. theorem OAI.MetricKMedian.FiniteComparison.actualB_nonneg line 21
  5. theorem OAI.MetricKMedian.FiniteComparison.proxy_N line 26
  6. theorem OAI.MetricKMedian.FiniteComparison.actual_first line 31
  7. theorem OAI.MetricKMedian.FiniteComparison.actual_L line 40
  8. theorem OAI.MetricKMedian.FiniteComparison.actual_linear line 58
  9. theorem OAI.MetricKMedian.FiniteComparison.actual_P_small line 77
  10. theorem OAI.MetricKMedian.FiniteComparison.kappa_absorb line 85
  11. theorem OAI.MetricKMedian.FiniteComparison.actual_final_bounds line 104
  12. theorem OAI.MetricKMedian.FiniteComparison.actual_charge_proxy line 147
  13. theorem OAI.MetricKMedian.FiniteComparison.actual_charge line 176
  14. theorem OAI.MetricKMedian.FiniteComparison.actual_scalar_bounds line 202
  15. theorem OAI.MetricKMedian.FiniteComparison.finite_comparison line 228