OAI/Combinatorics/KMedian/Process/Taper.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Taper.marginal line 9
  2. theorem OAI.MetricKMedian.Taper.marginal_nonneg line 11
  3. theorem OAI.MetricKMedian.Taper.marginal_le_one line 14
  4. theorem OAI.MetricKMedian.Taper.marginal_antitone line 16
  5. theorem OAI.MetricKMedian.Taper.marginal_one line 23
  6. theorem OAI.MetricKMedian.Taper.marginal_zero line 29
  7. theorem OAI.MetricKMedian.Taper.marginal_at_zero_distance line 33
  8. theorem OAI.MetricKMedian.Taper.lower_comparison line 37
  9. theorem OAI.MetricKMedian.Taper.upper_comparison line 49
  10. def OAI.MetricKMedian.Taper.mass line 64
  11. def OAI.MetricKMedian.Taper.colocatedMass line 66
  12. theorem OAI.MetricKMedian.Taper.mass_antitone line 68
  13. theorem OAI.MetricKMedian.Taper.continuous_mass line 73
  14. theorem OAI.MetricKMedian.Taper.exists_full_inverse line 77
  15. theorem OAI.MetricKMedian.Taper.exists_colocated_inverse line 93
  16. theorem OAI.MetricKMedian.Taper.exists_minimal_radius line 112