OAI/Combinatorics/KMedian/Expanders/ExpanderCompiler.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MetricKMedian.PCP.Compiler.Expander.sizePolyline 12 - lemma
OAI.MetricKMedian.PCP.Compiler.Expander.reachable_sizeline 15 - lemma
OAI.MetricKMedian.PCP.Compiler.Expander.poly_initialStateline 29 - lemma
OAI.MetricKMedian.PCP.Compiler.Expander.poly_stepsline 31 - lemma
OAI.MetricKMedian.PCP.Compiler.Expander.poly_trajectoryline 32 - lemma
OAI.MetricKMedian.PCP.Compiler.Expander.poly_generateline 41