OAI/Combinatorics/ParityLifts/SparseRates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParityWL.Complexity.densityFactor line 7
2. lemma OAI.ParityWL.Complexity.sparseDensity_eq line 9
3. lemma OAI.ParityWL.Complexity.ExpBound.polymul line 12
4. lemma OAI.ParityWL.Complexity.ExpBound.polypow line 15
5. lemma OAI.ParityWL.Complexity.sparseSize_rate line 18
6. lemma OAI.ParityWL.Complexity.ceilWidth_bound line 31
7. lemma OAI.ParityWL.Complexity.sparse_leafWords_bound line 41
8. lemma OAI.ParityWL.Complexity.ExpBound.affine_exp line 56
9. lemma OAI.ParityWL.Complexity.ExpBound.affine_exp_mul line 64
10. lemma OAI.ParityWL.Complexity.polynomial_program_rate line 71