OAI/Combinatorics/KMedian/Rounding/RationalPhysicalReplay.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.RationalPhysicalKernel.labels line 13
2. def OAI.MetricKMedian.RationalPhysicalKernel.replayList line 21
3. def OAI.MetricKMedian.RationalPhysicalKernel.replay line 27
4. theorem OAI.MetricKMedian.RationalPhysicalKernel.labels_subset line 32
5. theorem OAI.MetricKMedian.RationalPhysicalKernel.labels_active line 42
6. theorem OAI.MetricKMedian.RationalPhysicalKernel.replay_extend line 49
7. theorem OAI.MetricKMedian.RationalPhysicalKernel.replay_subset line 56
8. theorem OAI.MetricKMedian.RationalPhysicalKernel.histories_alive line 67