OAI/Computability/FourierTransform/Cost.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PowerSaving.Tape.ext_look line 12
2. theorem OAI.PowerSaving.Tape.len_tab line 22
3. theorem OAI.PowerSaving.Tape.look_tab line 24
4. theorem OAI.PowerSaving.Tape.len_set line 28
5. theorem OAI.PowerSaving.Tape.look_set_ne line 30
6. theorem OAI.PowerSaving.Tape.look_set_eq line 34
7. theorem OAI.PowerSaving.Tape.sow_zero line 37
8. theorem OAI.PowerSaving.Tape.sow_succ line 40
9. theorem OAI.PowerSaving.Tape.len_sow line 43
10. theorem OAI.PowerSaving.Tape.sow_look_written line 46
11. theorem OAI.PowerSaving.Tape.sow_consecutive line 61
12. structure OAI.PowerSaving.RAM.Bill.OK line 74

    Source documentation

    Evaluation guarantee.

    structure Bill.OK (b : Bill α) (x : α) (w p : ℕ) : Prop where
    …

    Mentions: OAI.PowerSaving.RAM.Bill

13. theorem OAI.PowerSaving.RAM.Bill.OK.mono line 84
14. theorem OAI.PowerSaving.RAM.Bill.OK.pass line 87
15. theorem OAI.PowerSaving.RAM.Bill.OK.pay line 93
16. theorem OAI.PowerSaving.RAM.Bill.one_ok line 97
17. theorem OAI.PowerSaving.RAM.Bill.word_ok line 100
18. theorem OAI.PowerSaving.RAM.Bill.steps_ok line 103
19. theorem OAI.PowerSaving.RAM.Bill.sow_ok line 115
20. theorem OAI.PowerSaving.RAM.Bill.tab_ok line 131