OAI/Computability/FourierTransform/FourierWords.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Fourier layer word. Correct on each axis at exact width, even when coincident intermediate wires hold arbitrary data.

  1. def OAI.PowerSaving.Slant.Creates line 11
  2. lemma OAI.PowerSaving.Slant.Creates.stack line 14
  3. lemma OAI.PowerSaving.Slant.creates_swatch line 19
  4. lemma OAI.PowerSaving.Slant.front_flows line 27
  5. def OAI.PowerSaving.Slant.echo line 31
  6. lemma OAI.PowerSaving.Slant.sound_echo line 33
  7. lemma OAI.PowerSaving.Slant.echo_go line 35
  8. def OAI.PowerSaving.Slant.coda line 38
  9. lemma OAI.PowerSaving.Slant.sound_coda line 40
  10. lemma OAI.PowerSaving.Slant.creep_coda line 43
  11. def OAI.PowerSaving.Slant.voices line 51
  12. def OAI.PowerSaving.Slant.repeatV line 54
  13. def OAI.PowerSaving.Slant.ode line 57
  14. def OAI.PowerSaving.Slant.ballad line 60
  15. lemma OAI.PowerSaving.Slant.sound_ode line 64
  16. lemma OAI.PowerSaving.Slant.beats_ode line 68
  17. lemma OAI.PowerSaving.Slant.fade_flip line 73
  18. lemma OAI.PowerSaving.Slant.creates_voices line 77
  19. lemma OAI.PowerSaving.Slant.creates_repeatV line 85
  20. lemma OAI.PowerSaving.Slant.creates_ode line 93
  21. lemma OAI.PowerSaving.Slant.sound_ballad line 101
  22. lemma OAI.PowerSaving.Slant.creates_ballad line 105
  23. def OAI.PowerSaving.Slant.score line 110
  24. lemma OAI.PowerSaving.Slant.beats_ballad line 112
  25. lemma OAI.PowerSaving.Slant.score_le line 117