OAI/Combinatorics/KMedian/Preparation/PreparationParameters.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Preparation.farFactor line 9
  2. def OAI.MetricKMedian.Preparation.shortfallFactor line 11
  3. def OAI.MetricKMedian.Preparation.nearFactor line 13
  4. def OAI.MetricKMedian.Preparation.failureFactor line 15
  5. def OAI.MetricKMedian.Preparation.parameterEnvelopeFar line 16
  6. def OAI.MetricKMedian.Preparation.parameterEnvelopeNear line 18
  7. def OAI.MetricKMedian.Preparation.parameterEnvelope line 20
  8. theorem OAI.MetricKMedian.Preparation.parameter_envelope_bounds line 23
  9. theorem OAI.MetricKMedian.Preparation.parameter_envelope_continuous line 74
  10. theorem OAI.MetricKMedian.Preparation.parameter_envelope_zero line 78
  11. theorem OAI.MetricKMedian.Preparation.exists_preparation_parameters line 81
  12. theorem OAI.MetricKMedian.Preparation.all_fine_grids line 137