OAI/Combinatorics/KMedian/Machines/Iteration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Amplifier.Box.next line 17
2. lemma OAI.MetricKMedian.PCP.Amplifier.Box.next_complete line 18
3. lemma OAI.MetricKMedian.PCP.Amplifier.Box.next_sound line 21
4. lemma OAI.MetricKMedian.PCP.Amplifier.Box.next_edges line 25
5. lemma OAI.MetricKMedian.PCP.Amplifier.Box.next_size line 29
6. def OAI.MetricKMedian.PCP.Amplifier.Box.iterate line 34
7. lemma OAI.MetricKMedian.PCP.Amplifier.Box.iterate_complete line 37
8. lemma OAI.MetricKMedian.PCP.Amplifier.Box.iterate_sound line 41
9. lemma OAI.MetricKMedian.PCP.Amplifier.Box.iterate_edges line 58
10. lemma OAI.MetricKMedian.PCP.Amplifier.Box.iterate_size line 67
11. lemma OAI.MetricKMedian.PCP.Amplifier.Box.inverse_edge_gap line 75
12. def OAI.MetricKMedian.PCP.Amplifier.Box.count line 85
13. def OAI.MetricKMedian.PCP.Amplifier.Box.amplified line 86
14. lemma OAI.MetricKMedian.PCP.Amplifier.Box.amplified_complete line 87
15. lemma OAI.MetricKMedian.PCP.Amplifier.Box.amplified_sound line 88