OAI/Computability/FourierTransform/DisjointIntervals.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Word primitives across equal disjoint intervals. Uniform shear realizations.

  1. def OAI.PowerSaving.Slant.shade line 11

    Source comment

    aligned spells with coordinates u and v
    def shade (u v : Zone) (f g : Line) : Reel :=
…

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

  2. def OAI.PowerSaving.Slant.jumps line 15
  3. def OAI.PowerSaving.Slant.snap line 19
  4. theorem OAI.PowerSaving.Slant.sound_shade line 21
  5. lemma OAI.PowerSaving.Slant.jumps_u line 29
  6. lemma OAI.PowerSaving.Slant.jumps_v line 32
  7. lemma OAI.PowerSaving.Slant.sound_snap line 36
  8. abbrev OAI.PowerSaving.Slant.Bicolor line 63
  9. def OAI.PowerSaving.Slant.twinsAt line 65
  10. structure OAI.PowerSaving.Slant.Twins line 67
  11. lemma OAI.PowerSaving.Slant.Twins.stack line 71
  12. lemma OAI.PowerSaving.Slant.Twins.congr line 76
  13. lemma OAI.PowerSaving.Slant.twins_shade line 86
  14. lemma OAI.PowerSaving.Slant.twins_snap line 96
  15. def OAI.PowerSaving.Slant.hinge line 111
  16. def OAI.PowerSaving.Slant.brick line 115
  17. def OAI.PowerSaving.Slant.spark line 120

    Source documentation

    Shear strong when f ≠ 0.

    def spark (u v : Zone) (f : Line) : Reel :=
…

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

  18. def OAI.PowerSaving.Slant.blaze line 124
  19. def OAI.PowerSaving.Slant.flash line 127

    Source documentation

    Avoid a coefficient zero test: uniform word for adding f*src.

    def flash (dst src : Zone) (f : Line) : Reel :=
…

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

  20. lemma OAI.PowerSaving.Slant.sound_hinge line 136
  21. lemma OAI.PowerSaving.Slant.sound_brick line 139
  22. lemma OAI.PowerSaving.Slant.sound_spark line 143
  23. lemma OAI.PowerSaving.Slant.sound_flash line 146
  24. lemma OAI.PowerSaving.Slant.twins_hinge line 151
  25. lemma OAI.PowerSaving.Slant.twins_brick line 161
  26. lemma OAI.PowerSaving.Slant.twins_spark line 169
  27. lemma OAI.PowerSaving.Slant.blaze_ne line 183
  28. lemma OAI.PowerSaving.Slant.after_ne line 190
  29. lemma OAI.PowerSaving.Slant.twins_flash line 199
  30. lemma OAI.PowerSaving.Slant.spill_flash line 209
  31. lemma OAI.PowerSaving.Slant.beats_shade line 223
  32. lemma OAI.PowerSaving.Slant.beats_snap line 224
  33. lemma OAI.PowerSaving.Slant.beats_hinge line 225
  34. lemma OAI.PowerSaving.Slant.beats_brick line 226
  35. lemma OAI.PowerSaving.Slant.beats_spark line 227
  36. lemma OAI.PowerSaving.Slant.beats_flash line 228