OAI/Combinatorics/KMedianRecovery/Encoding/LabelRange.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.ColorLabel.labelRange line 7
  2. def OAI.MetricKMedianRecovery.ColorLabel.label line 9
  3. lemma OAI.MetricKMedianRecovery.ColorLabel.labelRange_bounds line 12
  4. def OAI.MetricKMedianRecovery.ColorLabel.labelMass line 26
  5. lemma OAI.MetricKMedianRecovery.ColorLabel.labelMass_nonneg line 29
  6. lemma OAI.MetricKMedianRecovery.ColorLabel.labelMass_total line 33
  7. lemma OAI.MetricKMedianRecovery.ColorLabel.labelMass_lower line 43
  8. lemma OAI.MetricKMedianRecovery.ColorLabel.factorial_probability line 58
  9. def OAI.MetricKMedianRecovery.ColorLabel.distinctMass line 72
  10. lemma OAI.MetricKMedianRecovery.ColorLabel.distinctMass_lower line 76
  11. lemma OAI.MetricKMedianRecovery.ColorLabel.actual_distinct_probability line 100
  12. lemma OAI.MetricKMedianRecovery.ColorLabel.distinctMass_zero line 106
  13. lemma OAI.MetricKMedianRecovery.ColorLabel.product_event line 109
  14. def OAI.MetricKMedianRecovery.ColorLabel.color line 118
  15. def OAI.MetricKMedianRecovery.ColorLabel.colorMass line 121
  16. lemma OAI.MetricKMedianRecovery.ColorLabel.colorMass_values line 124
  17. lemma OAI.MetricKMedianRecovery.ColorLabel.colorMass_lower line 130
  18. lemma OAI.MetricKMedianRecovery.ColorLabel.colorMass_total line 134
  19. lemma OAI.MetricKMedianRecovery.ColorLabel.specified_color_probability line 137
  20. lemma OAI.MetricKMedianRecovery.ColorLabel.favorable_color_probability line 165
  21. lemma OAI.MetricKMedianRecovery.ColorLabel.event_pushforward line 173
  22. def OAI.MetricKMedianRecovery.ColorLabel.binaryDistinctMass line 195
  23. lemma OAI.MetricKMedianRecovery.ColorLabel.binaryDistinctMass_eq line 200
  24. lemma OAI.MetricKMedianRecovery.ColorLabel.binary_distinct_probability line 218