OAI/Computability/FourierTransform/BinaryFrames.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Fourier frames on one binary column. We use tensor Hadamard for matrix identities only. All executed scalar constants are in Q(i).

  1. def OAI.PowerSaving.Binary.sign line 11
  2. def OAI.PowerSaving.Binary.tint line 12
  3. lemma OAI.PowerSaving.Binary.sign_add line 14
  4. lemma OAI.PowerSaving.Binary.sign_sq line 18
  5. lemma OAI.PowerSaving.Binary.tint_add line 21
  6. lemma OAI.PowerSaving.Binary.tint_sq line 25
  7. lemma OAI.PowerSaving.Binary.sign_sum line 28
  8. def OAI.PowerSaving.Binary.lum line 37
  9. lemma OAI.PowerSaving.Binary.lum_zero line 39
  10. lemma OAI.PowerSaving.Binary.lum_add line 42
  11. lemma OAI.PowerSaving.Binary.lum_sq line 46
  12. lemma OAI.PowerSaving.Binary.lum_nonzero line 52
  13. lemma OAI.PowerSaving.Binary.lum_of_unit line 58
  14. def OAI.PowerSaving.Binary.littleH line 63
  15. def OAI.PowerSaving.Binary.littleH' line 65
  16. def OAI.PowerSaving.Binary.ca line 67
  17. def OAI.PowerSaving.Binary.cb line 68
  18. def OAI.PowerSaving.Binary.littleC line 69
  19. lemma OAI.PowerSaving.Binary.sum_bits line 71
  20. lemma OAI.PowerSaving.Binary.littleH_H' line 77
  21. lemma OAI.PowerSaving.Binary.little_phase line 83
  22. abbrev OAI.PowerSaving.Binary.CMat line 90
  23. def OAI.PowerSaving.Binary.kernel line 92
  24. def OAI.PowerSaving.Binary.wal line 94
  25. def OAI.PowerSaving.Binary.walI line 95
  26. lemma OAI.PowerSaving.Binary.wal_apply line 97
  27. lemma OAI.PowerSaving.Binary.wal_right line 102
  28. lemma OAI.PowerSaving.Binary.wal_left line 105
  29. def OAI.PowerSaving.Binary.wrap line 108
  30. lemma OAI.PowerSaving.Binary.wrap_of line 110
  31. lemma OAI.PowerSaving.Binary.wrap_one line 114
  32. lemma OAI.PowerSaving.Binary.wrap_mul line 117
  33. lemma OAI.PowerSaving.Binary.wrap_comm line 126
  34. lemma OAI.PowerSaving.Binary.wrap_lum line 129
  35. def OAI.PowerSaving.Binary.shift line 137
  36. lemma OAI.PowerSaving.Binary.shift_phase line 140
  37. lemma OAI.PowerSaving.Binary.shift_sq line 147
  38. def OAI.PowerSaving.Binary.dir line 152

    Source documentation

    Forward directional factor.

    def dir (z : Space α) : CMat α := ca • 1 + cb • shift z

    Mentions: OAI.PowerSaving.Binary.Space, OAI.PowerSaving.Binary.CMat, OAI.PowerSaving.Binary.ca, OAI.PowerSaving.Binary.cb, OAI.PowerSaving.Binary.shift

  39. lemma OAI.PowerSaving.Binary.dir_phase line 154
  40. lemma OAI.PowerSaving.Binary.dir_sq line 165
  41. def OAI.PowerSaving.Binary.frame line 169

    Source documentation

    Basis independent frame from projection.

    def frame (A : OBase α) (s : Finset α) := wrap fun x => lum (A.proj s x)

    Mentions: OAI.PowerSaving.Binary.OBase, OAI.PowerSaving.Binary.wrap, OAI.PowerSaving.Binary.lum

  42. lemma OAI.PowerSaving.Binary.frame_univ line 171
  43. lemma OAI.PowerSaving.Binary.frame_zero line 174
  44. lemma OAI.PowerSaving.Binary.frame_congr line 177
  45. def OAI.PowerSaving.Binary.unframe line 182

    Source documentation

    Frames are invertible (so cancellation along a path suffices).

    def unframe (A : OBase α) (s : Finset α) := wrap fun x => (lum (A.proj s x))⁻¹

    Mentions: OAI.PowerSaving.Binary.OBase, OAI.PowerSaving.Binary.wrap, OAI.PowerSaving.Binary.lum

  46. lemma OAI.PowerSaving.Binary.unframe_right line 184
  47. lemma OAI.PowerSaving.Binary.unframe_left line 188
  48. def OAI.PowerSaving.Binary.delta line 192

    Source documentation

    Change when adding one orthogonal line in a fixed mask.

    def delta (z : Space α) := wrap fun x => lum (dot z x • z)

    Mentions: OAI.PowerSaving.Binary.Space, OAI.PowerSaving.Binary.wrap, OAI.PowerSaving.Binary.lum, OAI.PowerSaving.Binary.dot

  49. lemma OAI.PowerSaving.Binary.frame_ins line 194
  50. lemma OAI.PowerSaving.Binary.delta_pos line 204
  51. lemma OAI.PowerSaving.Binary.delta_neg line 211
  52. lemma OAI.PowerSaving.Binary.delta_sq line 218
  53. lemma OAI.PowerSaving.Binary.delta_comm line 226
  54. lemma OAI.PowerSaving.Binary.delta_shift_comm line 230
  55. lemma OAI.PowerSaving.Binary.frame_shift_comm line 233