OAI/Analysis/MatrixSigning/Complexity/PolynomialLoops.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Realization.len_listCode line 15
2. lemma OAI.CurrentKS.Realization.sum_map_bound line 20
3. lemma OAI.CurrentKS.Realization.listCode_length_bound line 29
4. lemma OAI.CurrentKS.Realization.list_length_le_code line 36
5. lemma OAI.CurrentKS.Realization.mem_length_le_code line 40
6. lemma OAI.CurrentKS.Realization.listCode_reverse_length line 51
7. instance OAI.CurrentKS.Realization.poly_map line 55
8. lemma OAI.CurrentKS.Realization.fold_scan_bound line 83
9. class OAI.CurrentKS.Realization.FoldSize line 103
10. instance OAI.CurrentKS.Realization.poly_fold line 107
11. lemma OAI.CurrentKS.Realization.iterate_ticks_bound line 137
12. class OAI.CurrentKS.Realization.IterateSize line 150
13. instance OAI.CurrentKS.Realization.poly_iterate line 152