OAI/Combinatorics/KMedian/Preparation/RepresentativeProgram.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.Input line 15
  2. abbrev OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.Raw line 21
  3. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.Input.raw line 22
  4. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.Input.encode line 23
  5. abbrev OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.Cut line 24
  6. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.advance line 25
  7. structure OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.State line 30
  8. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.State.raw line 33
  9. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.State.encode line 34
  10. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.State.step line 35
  11. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.Input.state line 36
  12. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.Input.start line 37
  13. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.stepRaw line 39
  14. theorem OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.stepRaw_poly line 46
  15. theorem OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.any_view line 54
  16. theorem OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.stepRaw_state line 61
  17. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.stepProgram line 83
  18. theorem OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.state_iterate line 85
  19. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.startProgram line 93
  20. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.countProgram line 104
  21. theorem OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.input_bound line 107
  22. theorem OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.mask_length line 114
  23. theorem OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.state_size line 115
  24. theorem OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.select_empty line 126
  25. theorem OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.advance_result line 128
  26. def OAI.MetricKMedian.Preparation.RationalRepresentatives.Program.program line 142