OAI/Combinatorics/ParityLifts/SparseStep.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Sparsification.split_from_two line 9
2. lemma OAI.Sparsification.split_from_three_binary line 22
3. lemma OAI.Sparsification.split_from_three_unit line 36
4. abbrev OAI.ParityWL.Complexity.SparseResult line 55
5. def OAI.ParityWL.Complexity.sparseBranch line 57
6. def OAI.ParityWL.Complexity.sparseStep line 60
7. lemma OAI.ParityWL.Complexity.sparseStep_spec line 68
8. def OAI.ParityWL.Complexity.PolyProgram.sparseBranch line 111
9. def OAI.ParityWL.Complexity.PolyProgram.sparseStep line 120