OAI/Combinatorics/KMedian/Expanders/ExpanderTables.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MetricKMedian.PCP.Compiler.Expander.next_tableline 13 - def
OAI.MetricKMedian.PCP.Compiler.Expander.initialline 39 - lemma
OAI.MetricKMedian.PCP.Compiler.Expander.iterate_sequenceline 40 - lemma
OAI.MetricKMedian.PCP.Compiler.Expander.iterate_tableline 45