OAI/Computability/FourierTransform/LayerWords.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Layer words using the binary kernel copies and scaled-index layers. Exact-width by a closure property on indices touched (indices outside the width never used and are identity). Arrays modeled on ℕ. Monomial-slot representation doesn't need a permutation certificate; it works even for a "gather".

  1. structure OAI.PowerSaving.Slant.Stroke line 15
  2. def OAI.PowerSaving.Slant.Stroke.applyM line 22
  3. def OAI.PowerSaving.Slant.Stroke.applyC line 24
  4. def OAI.PowerSaving.Slant.Stroke.send line 27
  5. structure OAI.PowerSaving.Slant.Stroke.Sound line 29
  6. lemma OAI.PowerSaving.Slant.Stroke.Sound.wider line 40
  7. theorem OAI.PowerSaving.Slant.Stroke.Sound.same line 50
  8. theorem OAI.PowerSaving.Slant.Stroke.Sound.send_congr line 53
  9. def OAI.PowerSaving.Slant.Stroke.unmark line 62
  10. theorem OAI.PowerSaving.Slant.Stroke.send_unmark line 64
  11. theorem OAI.PowerSaving.Slant.Stroke.sound_unmark line 66
  12. def OAI.PowerSaving.Slant.Stroke.plain line 70

    Source documentation

    A scaled lookup; used for monomial slots.

    def plain (n : ℕ) (l : ℕ→ℕ) (d : Line) : Stroke :=
…

    Mentions: OAI.PowerSaving.Line, OAI.PowerSaving.Slant.Stroke

  13. theorem OAI.PowerSaving.Slant.Stroke.plain_sound line 73
  14. theorem OAI.PowerSaving.Slant.Stroke.plain_send line 78
  15. def OAI.PowerSaving.Slant.Stroke.beside line 83

    Source comment

    parallel sum
    def beside (p : ℕ) (u v : Stroke) : Stroke where
…

    Mentions: OAI.PowerSaving.Slant.Stroke

  16. theorem OAI.PowerSaving.Slant.Stroke.Sound.beside line 88
  17. def OAI.PowerSaving.Slant.Stroke.drift line 118
  18. theorem OAI.PowerSaving.Slant.Stroke.beside_left line 120
  19. theorem OAI.PowerSaving.Slant.Stroke.beside_right line 124
  20. structure OAI.PowerSaving.Slant.Reel line 134

    Source documentation

    Array of strokes; slots read for t < beats.

    structure Reel where
…
  21. def OAI.PowerSaving.Slant.Reel.reach line 140
  22. def OAI.PowerSaving.Slant.Reel.go line 144
  23. def OAI.PowerSaving.Slant.Reel.Sound line 146
  24. lemma OAI.PowerSaving.Slant.Reel.Sound.wider line 152
  25. theorem OAI.PowerSaving.Slant.Reel.Sound.still line 155
  26. theorem OAI.PowerSaving.Slant.Reel.Sound.go_congr line 165
  27. def OAI.PowerSaving.Slant.Reel.wait line 176
  28. theorem OAI.PowerSaving.Slant.Reel.go_wait line 178
  29. theorem OAI.PowerSaving.Slant.Reel.sound_wait line 183
  30. def OAI.PowerSaving.Slant.Reel.tick line 185
  31. theorem OAI.PowerSaving.Slant.Reel.go_tick line 187
  32. lemma OAI.PowerSaving.Slant.Reel.sound_tick line 190
  33. def OAI.PowerSaving.Slant.Reel.stack line 193

    Source documentation

    Stack layer sequences, a performed first.

    def stack (a b : Reel) : Reel :=
…

    Mentions: OAI.PowerSaving.Slant.Reel

  34. lemma OAI.PowerSaving.Slant.Reel.go_stack line 196
  35. lemma OAI.PowerSaving.Slant.Reel.Sound.stack line 214
  36. def OAI.PowerSaving.Slant.Reel.parallel line 223

    Source documentation

    zip in parallel; used with matching lengths.

    def parallel (p : ℕ) (a b : Reel) : Reel :=
…

    Mentions: OAI.PowerSaving.Slant.Reel

  37. theorem OAI.PowerSaving.Slant.Reel.Sound.parallel line 226
  38. theorem OAI.PowerSaving.Slant.Reel.parallel_left line 231
  39. theorem OAI.PowerSaving.Slant.Reel.parallel_right line 243
  40. def OAI.PowerSaving.Slant.Reel.atBase line 254

    Source documentation

    Use at offset p.

    def atBase (p : ℕ) (a : Reel) : Reel := parallel p (wait a.beats) a

    Mentions: OAI.PowerSaving.Slant.Reel, OAI.PowerSaving.Slant.Reel.parallel, OAI.PowerSaving.Slant.Reel.wait

  41. lemma OAI.PowerSaving.Slant.Reel.Sound.atBase line 256
  42. lemma OAI.PowerSaving.Slant.Reel.atBase_left line 260
  43. lemma OAI.PowerSaving.Slant.Reel.atBase_right line 264
  44. def OAI.PowerSaving.Slant.Reel.swatch line 269

    Source comment

    layer singleton builders
    def swatch (n : ℕ) (d : Line) : Reel :=
…

    Mentions: OAI.PowerSaving.Line, OAI.PowerSaving.Slant.Reel

  45. def OAI.PowerSaving.Slant.Reel.lace line 272
  46. lemma OAI.PowerSaving.Slant.Reel.sound_swatch line 275
  47. lemma OAI.PowerSaving.Slant.Reel.go_swatch line 278
  48. lemma OAI.PowerSaving.Slant.Reel.sound_lace line 282
  49. lemma OAI.PowerSaving.Slant.Reel.go_lace line 285