OAI/Computability/FourierTransform/ToeplitzLayers.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Dyadic exact-width layers for lower triangular Toeplitz.

  1. def OAI.PowerSaving.Slant.reachSize line 10
  2. def OAI.PowerSaving.Slant.bridgeSpan line 14
  3. def OAI.PowerSaving.Slant.Springs line 17
  4. lemma OAI.PowerSaving.Slant.beats_span line 20
  5. lemma OAI.PowerSaving.Slant.desc_num line 26
  6. lemma OAI.PowerSaving.Slant.sound_span line 30
  7. lemma OAI.PowerSaving.Slant.spill_span line 39
  8. lemma OAI.PowerSaving.Slant.reach_le line 47
  9. def OAI.PowerSaving.Slant.chorus line 54
  10. def OAI.PowerSaving.Slant.hoop line 58
  11. def OAI.PowerSaving.Slant.harp line 63
  12. lemma OAI.PowerSaving.Slant.beats_hoop line 67
  13. lemma OAI.PowerSaving.Slant.beats_harp line 74
  14. lemma OAI.PowerSaving.Slant.chorus_le line 81
  15. lemma OAI.PowerSaving.Slant.sound_hoop line 90
  16. lemma OAI.PowerSaving.Slant.branch_smaller line 103
  17. lemma OAI.PowerSaving.Slant.sound_harp line 106
  18. lemma OAI.PowerSaving.Slant.spill_after line 117
  19. lemma OAI.PowerSaving.Slant.flows_hoop line 148
  20. lemma OAI.PowerSaving.Slant.flows_harp line 168