OAI/Computability/FourierTransform/IntegerPrograms.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PowerSaving.RAM.Small.sub line 15
2. theorem OAI.PowerSaving.RAM.Small.div line 18
3. theorem OAI.PowerSaving.RAM.Small.mod line 21
4. lemma OAI.PowerSaving.RAM.Can.minus line 28
5. lemma OAI.PowerSaving.RAM.Can.times line 32
6. lemma OAI.PowerSaving.RAM.Can.plus line 36
7. lemma OAI.PowerSaving.RAM.Can.dvdW line 40
8. lemma OAI.PowerSaving.RAM.Can.modW line 44
9. lemma OAI.PowerSaving.RAM.Can.wpow_fixed line 48
10. lemma OAI.PowerSaving.RAM.Can.wTwo line 55

    Source documentation

    Cost-sensitive powering of two to a variable exponent by doubling.

    lemma wTwo (h : Can m B s w x A W) (hh : Small B A)
        (hq : Small B fun i => 2^A i) (ha : Dom W A) :
        Can m B s w x (fun i => 2^A i) W := by
    …

    Mentions: OAI.PowerSaving.RAM.Can, OAI.PowerSaving.RAM.Small, OAI.PowerSaving.RAM.Dom

11. lemma OAI.PowerSaving.RAM.Can.neg line 77
12. lemma OAI.PowerSaving.RAM.Can.cNat line 81
13. lemma OAI.PowerSaving.RAM.Can.cInt line 88
14. lemma OAI.PowerSaving.RAM.Can.rat line 95
15. lemma OAI.PowerSaving.RAM.Can.cpow_fixed line 100
16. lemma OAI.PowerSaving.RAM.Can.prod_cconst line 108
17. lemma OAI.PowerSaving.RAM.Can.addr_join line 130
18. lemma OAI.PowerSaving.RAM.Can.addr_high line 139
19. lemma OAI.PowerSaving.RAM.Can.addr_low line 146