OAI/Combinatorics/KMedianRecovery/Refined/CheckedInput.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.n line 14
  2. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.distance line 15
  3. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.mask line 16
  4. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.rows line 18
  5. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.metricTest line 20
  6. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.valid line 28
  7. theorem OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.distance_poly line 31
  8. theorem OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.rows_poly line 36
  9. theorem OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.bool_beq_poly line 39
  10. theorem OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.valid_poly line 48
  11. lemma OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.mask_card line 52
  12. lemma OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.metricTest_spec line 63
  13. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.ofValid line 74
  14. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.fallback line 89
  15. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.checked line 102
  16. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.normalized line 104
  17. theorem OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.normalized_poly line 108
  18. lemma OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.mask_view line 112
  19. lemma OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.range_map line 119
  20. lemma OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.normalized_view line 123
  21. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.program line 133
  22. lemma OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.distance_view line 143
  23. lemma OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.valid_view line 147
  24. lemma OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.view_injective line 180
  25. lemma OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.checked_view line 204
  26. def OAI.MetricKMedianRecovery.RefinedRecovery.CheckedInput.parseProgram line 209