OAI/Combinatorics/KMedian/Rounding/RationalTaperZero.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Taper.extend line 12
  2. theorem OAI.MetricKMedian.Taper.extend_spec line 16
  3. def OAI.MetricKMedian.Taper.zeroSources line 35
  4. def OAI.MetricKMedian.Taper.zeroSelection line 37
  5. def OAI.MetricKMedian.Taper.zeroMarginal line 40
  6. theorem OAI.MetricKMedian.Taper.zero_data line 43