OAI/Computability/FourierTransform/ToeplitzUpdates.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Addition of a Toeplitz block by routing through a large enough circulant.

  1. def OAI.PowerSaving.Slant.trail line 11
  2. def OAI.PowerSaving.Slant.slice line 14
  3. def OAI.PowerSaving.Slant.pad line 17
  4. def OAI.PowerSaving.Slant.trim line 20
  5. lemma OAI.PowerSaving.Slant.Reads.chain line 22
  6. lemma OAI.PowerSaving.Slant.reads_pad line 26
  7. lemma OAI.PowerSaving.Slant.reads_trim line 33
  8. lemma OAI.PowerSaving.Slant.additive_trim line 36
  9. lemma OAI.PowerSaving.Slant.pad_neg line 39
  10. lemma OAI.PowerSaving.Slant.trim_neg line 43
  11. lemma OAI.PowerSaving.Slant.broader_pad line 47
  12. lemma OAI.PowerSaving.Slant.broader_trim line 61
  13. lemma OAI.PowerSaving.Slant.sound_trail line 69
  14. lemma OAI.PowerSaving.Slant.sound_slice line 73
  15. lemma OAI.PowerSaving.Slant.spill_trail line 77
  16. lemma OAI.PowerSaving.Slant.spill_slice line 82
  17. def OAI.PowerSaving.Slant.duct line 89
  18. def OAI.PowerSaving.Slant.well line 93
  19. lemma OAI.PowerSaving.Slant.beats_cameo line 97
  20. lemma OAI.PowerSaving.Slant.beats_duct line 99
  21. lemma OAI.PowerSaving.Slant.beats_well line 102
  22. lemma OAI.PowerSaving.Slant.sound_duct line 114
  23. lemma OAI.PowerSaving.Slant.spill_duct line 120
  24. lemma OAI.PowerSaving.Slant.sound_well line 135
  25. lemma OAI.PowerSaving.Slant.spill_well line 141
  26. def OAI.PowerSaving.Slant.spout line 161

    Source comment

    logical lower Toeplitz between offsets l (source), m (target), in different physical chunks.
    def spout (e l m : ℕ) (h : Line) (x : Line) : Line :=
…

    Mentions: OAI.PowerSaving.Line

  27. def OAI.PowerSaving.Slant.skirt line 166

    Source documentation

    2*b slots. k < b for positive or zero displacement. Leave non-required displacements 0 for convenience -- coefficients beyond the supplied span need not be evaluated.

    def skirt (b e s l m : ℕ) (h : Line) : Line :=
…

    Mentions: OAI.PowerSaving.Line

  28. lemma OAI.PowerSaving.Slant.skirt_spec line 173
  29. lemma OAI.PowerSaving.Slant.trim_spout line 185
  30. lemma OAI.PowerSaving.Slant.reads_spout line 200
  31. lemma OAI.PowerSaving.Slant.additive_spout line 203
  32. lemma OAI.PowerSaving.Slant.spout_neg line 207
  33. def OAI.PowerSaving.Slant.bore line 214
  34. lemma OAI.PowerSaving.Slant.beats_bore line 217
  35. lemma OAI.PowerSaving.Slant.sound_bore line 229
  36. lemma OAI.PowerSaving.Slant.spill_bore line 234