OAI/Combinatorics/KMedian/Amplification/PowerPrograms.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.MetricKMedian.PCP.Compiler.PowerProgram.Tagline 18 - def
OAI.MetricKMedian.PCP.Compiler.PowerProgram.stopline 19 - def
OAI.MetricKMedian.PCP.Compiler.PowerProgram.relsline 21 - lemma
OAI.MetricKMedian.PCP.Compiler.PowerProgram.poly_relsline 25 - def
OAI.MetricKMedian.PCP.Compiler.PowerProgram.rowline 30 - lemma
OAI.MetricKMedian.PCP.Compiler.PowerProgram.poly_rowline 35