OAI/Combinatorics/KMedian/Process/SourceGenerator.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.FixedBatch.graphActions line 14
2. theorem OAI.MetricKMedian.FixedBatch.mem_graph_erase line 19
3. theorem OAI.MetricKMedian.FixedBatch.indicator_sum line 22
4. theorem OAI.MetricKMedian.FixedBatch.nonindicator_sum line 31
5. theorem OAI.MetricKMedian.FixedBatch.graph_removed_mass line 43
6. theorem OAI.MetricKMedian.FixedBatch.graph_removed_cost line 48
7. theorem OAI.MetricKMedian.FixedBatch.source_generator_identity line 52