OAI/Computability/FourierTransform/BitLayout.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PowerSaving.Binary.Bits line 11
  2. def OAI.PowerSaving.Binary.lbit line 13
  3. def OAI.PowerSaving.Binary.shape line 26
  4. def OAI.PowerSaving.Binary.bits line 28
  5. theorem OAI.PowerSaving.Binary.bit_len line 30
  6. theorem OAI.PowerSaving.Binary.bits_len line 32
  7. theorem OAI.PowerSaving.Binary.bits_loc line 34
  8. theorem OAI.PowerSaving.Binary.bits_div line 37
  9. theorem OAI.PowerSaving.Binary.bits_lit line 40
  10. abbrev OAI.PowerSaving.Binary.Layers line 52

    Source comment

    Amplification axes. First come all m groups whose f-bit digit is indexed by one of α. These are followed by r spectator axes.
    abbrev Layers (α : Type*) (r f : ℕ) := (α × Fin f) ⊕ Fin r
  11. def OAI.PowerSaving.Binary.stick line 53
  12. abbrev OAI.PowerSaving.Binary.Grid line 56
  13. def OAI.PowerSaving.Binary.rows line 58
  14. def OAI.PowerSaving.Binary.bodyOrder line 65

    Source documentation

    Slow spectator, then column positions in α each with an f-bit digit.

    def bodyOrder (X : Layout α) (f : ℕ) : Layout (Sky α f) :=
…

    Mentions: OAI.PowerSaving.Layout, OAI.PowerSaving.Binary.Sky

  15. def OAI.PowerSaving.Binary.book line 68
  16. theorem OAI.PowerSaving.Binary.stick_len line 71
  17. theorem OAI.PowerSaving.Binary.book_len line 74
  18. def OAI.PowerSaving.Binary.build line 79
  19. theorem OAI.PowerSaving.Binary.book_code line 87
  20. def OAI.PowerSaving.Binary.normIndex line 105
  21. lemma OAI.PowerSaving.Binary.normIndex_val line 108
  22. lemma OAI.PowerSaving.Binary.normal_code line 111
  23. def OAI.PowerSaving.Binary.serial line 123
  24. lemma OAI.PowerSaving.Binary.serial_code line 127
  25. theorem OAI.PowerSaving.Binary.kernel_permute line 132
  26. lemma OAI.PowerSaving.Binary.kernel_build line 139
  27. lemma OAI.PowerSaving.Binary.kernel_serial line 149
  28. def OAI.PowerSaving.Binary.ripple line 156

    Source comment

    actValue convenience: kernel axes matrix times input
    def ripple (k : ℕ) (x : Bits k → ℂ) := kernel (Fin k) *ᵥ x

    Mentions: OAI.PowerSaving.Binary.Bits, OAI.PowerSaving.Binary.kernel

  29. def OAI.PowerSaving.Binary.chords line 158
  30. lemma OAI.PowerSaving.Binary.ripple_grid line 161