OAI/Combinatorics/KMedian/Amplification/AmplifierTableSize.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.rawCo line 12
2. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.rawCo_pos line 16
3. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.arithmetic line 18
4. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.raw_count line 27
5. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.raw_exists line 41
6. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.coefficient_exists line 50
7. def OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.co line 53
8. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.co_pos line 54
9. lemma OAI.MetricKMedian.PCP.Compiler.AmplifierProgram.next_count line 55