OAI/Computability/FourierTransform/ArbitraryLength.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PowerSaving.RAM.Bench.surf line 15
  2. lemma OAI.PowerSaving.RAM.Bench.surf_deg line 16
  3. def OAI.PowerSaving.RAM.Bench.Swift line 19
  4. lemma OAI.PowerSaving.RAM.Bench.Swift.of_moves line 24
  5. lemma OAI.PowerSaving.RAM.Bench.Swift.of_dry line 27
  6. lemma OAI.PowerSaving.RAM.Bench.Swift.pair line 30
  7. lemma OAI.PowerSaving.RAM.Bench.Swift.bind line 36
  8. def OAI.PowerSaving.RAM.Bench.tailVol line 44
  9. structure OAI.PowerSaving.RAM.Bench.Cruise line 46
  10. lemma OAI.PowerSaving.RAM.Bench.signP line 53
  11. lemma OAI.PowerSaving.RAM.Bench.table_scale line 59
  12. lemma OAI.PowerSaving.RAM.Bench.Cruise.transfer line 72
  13. lemma OAI.PowerSaving.RAM.Bench.Cruise.volume_ge line 76
  14. lemma OAI.PowerSaving.RAM.Bench.Cruise.volume_lt line 78
  15. lemma OAI.PowerSaving.RAM.Bench.Cruise.volume_pos line 80
  16. lemma OAI.PowerSaving.RAM.Bench.Cruise.dom line 83
  17. lemma OAI.PowerSaving.RAM.Bench.Cruise.flood line 86
  18. lemma OAI.PowerSaving.RAM.Bench.Cruise.flood' line 101
  19. lemma OAI.PowerSaving.RAM.Bench.Cruise.posts line 107
  20. lemma OAI.PowerSaving.RAM.Bench.Cruise.pearl line 119
  21. lemma OAI.PowerSaving.RAM.Bench.Cruise.risen line 128

    Source comment

    two prep arrays
    lemma risen (h : b.Cruise n S N) (r : Bool)
    (hp : b.Moves (fun _ => 0) (a sc) fun i => tablePow (pr r (2*n i)) (S i))
    (hx : b.Moves (fun _ => 0) (a (c cl)) fun i => Tape.tab (n i) (x i)) :
    b.Swift n S (a (c cl)) fun i => Tape.tab (N i) (chirp_seed (n i) (pr r (2*n i)) (x i)) := by
…

    Mentions: OAI.PowerSaving.RAM.sc, OAI.PowerSaving.RAM.Bench.tablePow, OAI.PowerSaving.Tape.tab

  22. lemma OAI.PowerSaving.RAM.Bench.Cruise.fallen line 141
  23. lemma OAI.PowerSaving.RAM.Bench.Cruise.pyramid line 156
  24. lemma OAI.PowerSaving.RAM.Bench.Cruise.singing line 174
  25. lemma OAI.PowerSaving.RAM.Bench.Cruise.deliver line 198
  26. lemma OAI.PowerSaving.RAM.Bench.Neaps.swift line 208