OAI/Combinatorics/KMedian/Rounding/RationalPhysicalKernel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RationalPhysicalKernel.copyOrder line 16
  2. def OAI.MetricKMedian.RationalPhysicalKernel.own line 24
  3. def OAI.MetricKMedian.RationalPhysicalKernel.enumeration line 27
  4. def OAI.MetricKMedian.RationalPhysicalKernel.graphLaw line 30
  5. abbrev OAI.MetricKMedian.RationalPhysicalKernel.Payload line 35
  6. abbrev OAI.MetricKMedian.RationalPhysicalKernel.State line 38
  7. def OAI.MetricKMedian.RationalPhysicalKernel.updateEvent line 41
  8. def OAI.MetricKMedian.RationalPhysicalKernel.step line 48
  9. theorem OAI.MetricKMedian.RationalPhysicalKernel.step_expectation line 56
  10. theorem OAI.MetricKMedian.RationalPhysicalKernel.step_records line 73
  11. def OAI.MetricKMedian.RationalPhysicalKernel.branching line 80
  12. theorem OAI.MetricKMedian.RationalPhysicalKernel.step_length line 84
  13. theorem OAI.MetricKMedian.RationalPhysicalKernel.branching_mono line 94
  14. theorem OAI.MetricKMedian.RationalPhysicalKernel.step_length_global line 98
  15. def OAI.MetricKMedian.RationalPhysicalKernel.histories line 107
  16. theorem OAI.MetricKMedian.RationalPhysicalKernel.histories_length line 113