OAI/Combinatorics/KMedianRecovery/Algorithms/GlobalRoundMetric.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.ceil_cast line 10
2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.round_edge line 15
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.duplicateMetric line 23
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.duplicate_dist line 25
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.left_injective line 27
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.right_injective line 31
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.card_left line 36
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.card_right line 37
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.dist_left_right line 38
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.connection_image line 42
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.cost_image line 62
12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.project_subset line 68
13. theorem OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalRounding.rounded_program line 87