OAI/Computability/FourierTransform/PolynomialPrograms.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PowerSaving.RAM.PolyCan line 12

    Source documentation

    One algorithm; time is polynomial in (S+2), integer bounds polynomial in (B+2). Often S polylogarithmic in B.

    def PolyCan {ι : Type U} (m : Bool) (B S : ι → ℕ) (s t) (x : ι → T s) (y : ι → T t) : Prop :=
…
  2. theorem OAI.PowerSaving.RAM.PolyCan.of_can line 21
  3. theorem OAI.PowerSaving.RAM.PolyCan.cong line 26
  4. theorem OAI.PowerSaving.RAM.PolyCan.reindex line 31
  5. theorem OAI.PowerSaving.RAM.PolyCan.poly_power line 36
  6. theorem OAI.PowerSaving.RAM.PolyCan.weaken line 39
  7. theorem OAI.PowerSaving.RAM.PolyCan.pipe line 44
  8. theorem OAI.PowerSaving.RAM.PolyCan.pair line 50
  9. theorem OAI.PowerSaving.RAM.PolyCan.bind line 56
  10. theorem OAI.PowerSaving.RAM.PolyCan.id line 63
  11. theorem OAI.PowerSaving.RAM.PolyCan.fst line 66
  12. theorem OAI.PowerSaving.RAM.PolyCan.snd line 71
  13. theorem OAI.PowerSaving.RAM.PolyCan.first line 76
  14. theorem OAI.PowerSaving.RAM.PolyCan.second line 79
  15. theorem OAI.PowerSaving.RAM.PolyCan.wc line 82
  16. theorem OAI.PowerSaving.RAM.PolyCan.zero line 84
  17. theorem OAI.PowerSaving.RAM.PolyCan.one line 86
  18. theorem OAI.PowerSaving.RAM.PolyCan.add line 90
  19. theorem OAI.PowerSaving.RAM.PolyCan.sub line 95
  20. theorem OAI.PowerSaving.RAM.PolyCan.mul line 100
  21. theorem OAI.PowerSaving.RAM.PolyCan.inv line 105
  22. theorem OAI.PowerSaving.RAM.PolyCan.look line 111
  23. theorem OAI.PowerSaving.RAM.PolyCan.len line 115
  24. theorem OAI.PowerSaving.RAM.PolyCan.wadd line 120
  25. theorem OAI.PowerSaving.RAM.PolyCan.wsub line 125
  26. theorem OAI.PowerSaving.RAM.PolyCan.wmul line 130
  27. theorem OAI.PowerSaving.RAM.PolyCan.wdiv line 135
  28. theorem OAI.PowerSaving.RAM.PolyCan.wmod line 140
  29. theorem OAI.PowerSaving.RAM.PolyCan.wlt line 145
  30. theorem OAI.PowerSaving.RAM.PolyCan.loop line 149
  31. theorem OAI.PowerSaving.RAM.PolyCan.tab line 163
  32. theorem OAI.PowerSaving.RAM.PolyCan.sow line 174
  33. theorem OAI.PowerSaving.RAM.PolyCan.testz line 188