OAI/Computability/FourierTransform/NetworkRoles.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Binary network with 32 coordinates. Triple indicators omit two fixed pivots. Unused ordered side pairs can also have storage assigned.

  1. abbrev OAI.PowerSaving.Cluster.H line 10
  2. abbrev OAI.PowerSaving.Cluster.J line 11
  3. abbrev OAI.PowerSaving.Cluster.Blocks line 12
  4. abbrev OAI.PowerSaving.Cluster.Mask line 13
  5. def OAI.PowerSaving.Cluster.freeSet line 14
  6. def OAI.PowerSaving.Cluster.tripSet line 15
  7. abbrev OAI.PowerSaving.Cluster.Trip line 16
  8. lemma OAI.PowerSaving.Cluster.piv line 18
  9. lemma OAI.PowerSaving.Cluster.trip_card line 20
  10. lemma OAI.PowerSaving.Cluster.trip_sub line 23
  11. lemma OAI.PowerSaving.Cluster.num_trip line 26
  12. def OAI.PowerSaving.Cluster.meet line 34
  13. def OAI.PowerSaving.Cluster.neighbor line 35
  14. instance OAI.PowerSaving.Cluster.(instance at line 36) line 36
  15. lemma OAI.PowerSaving.Cluster.meet_comm line 38
  16. lemma OAI.PowerSaving.Cluster.meet_self line 39
  17. lemma OAI.PowerSaving.Cluster.meet_le line 40
  18. lemma OAI.PowerSaving.Cluster.neighbor_comm line 51
  19. def OAI.PowerSaving.Cluster.tip line 54
  20. theorem OAI.PowerSaving.Cluster.meet_ind line 57

    Source documentation

    Also useful for scalar rows.

    theorem meet_ind {R : Type*} [Semiring R] (x y : Trip) :
    ∑ i : H, ((if i ∈ x.val then (1:R) else 0)*(if i ∈ y.val then 1 else 0))
    = (meet x y:R) := by
…

    Mentions: OAI.PowerSaving.Cluster.Trip, OAI.PowerSaving.Cluster.H, OAI.PowerSaving.Cluster.meet

  21. theorem OAI.PowerSaving.Cluster.tip_unit line 71
  22. theorem OAI.PowerSaving.Cluster.tip_zero line 76
  23. theorem OAI.PowerSaving.Cluster.tip_one line 79
  24. theorem OAI.PowerSaving.Cluster.tip_orth line 83
  25. def OAI.PowerSaving.Cluster.tripBase line 89
  26. theorem OAI.PowerSaving.Cluster.tripBase_main line 93
  27. theorem OAI.PowerSaving.Cluster.tripBase_unused line 95
  28. def OAI.PowerSaving.Cluster.pairBase line 98
  29. lemma OAI.PowerSaving.Cluster.pairBase_left line 103
  30. lemma OAI.PowerSaving.Cluster.pairBase_right line 110
  31. def OAI.PowerSaving.Cluster.sets line 118

    Source documentation

    Rectangles: free past if e=true, fixed zero otherwise; select S in the current axis; future fixed zero.

    def sets (j : J) (e : Bool) (s : Finset H) (i : J) : Finset H :=
…

    Mentions: OAI.PowerSaving.Cluster.J, OAI.PowerSaving.Cluster.H

  32. def OAI.PowerSaving.Cluster.rect line 121
  33. def OAI.PowerSaving.Cluster.future line 124
  34. def OAI.PowerSaving.Cluster.previous line 125
  35. lemma OAI.PowerSaving.Cluster.mem_rect line 127
  36. def OAI.PowerSaving.Cluster.big line 145

    Source comment

    Label abbreviations (at fixed j)
    def big (j : J) : Mask := rect j true univ

    Mentions: OAI.PowerSaving.Cluster.J, OAI.PowerSaving.Cluster.Mask, OAI.PowerSaving.Cluster.rect

  37. def OAI.PowerSaving.Cluster.belt line 146
  38. def OAI.PowerSaving.Cluster.xstart line 147
  39. def OAI.PowerSaving.Cluster.ystart line 148
  40. def OAI.PowerSaving.Cluster.xstep line 150

    Source documentation

    Big minus P tensor the complement of the slot.

    def xstep (j : J) (slot : H) : Mask := big j \ rect j false (univ \ {slot})

    Mentions: OAI.PowerSaving.Cluster.J, OAI.PowerSaving.Cluster.H, OAI.PowerSaving.Cluster.Mask, OAI.PowerSaving.Cluster.big, OAI.PowerSaving.Cluster.rect

  41. def OAI.PowerSaving.Cluster.ystep line 151
  42. theorem OAI.PowerSaving.Cluster.in_big line 153
  43. theorem OAI.PowerSaving.Cluster.in_belt line 154
  44. theorem OAI.PowerSaving.Cluster.in_xstart line 156
  45. theorem OAI.PowerSaving.Cluster.in_ystart line 158
  46. theorem OAI.PowerSaving.Cluster.in_xstep line 161
  47. theorem OAI.PowerSaving.Cluster.in_ystep line 164
  48. lemma OAI.PowerSaving.Cluster.rect_le_big line 168
  49. lemma OAI.PowerSaving.Cluster.belt_drop line 172
  50. lemma OAI.PowerSaving.Cluster.rect_proj line 187

    Source documentation

    Compare frames by comparing the current base projectors.

    lemma rect_proj {b d : J → OBase H} {j : J} {s t : Finset H}
    (hi : ∀ i, i ≠ j → b i = d i)
    (hh : (b j).mat s = (d j).mat t) (e : Bool) :
    (OBase.tensor b).mat (rect j e s) = (OBase.tensor d).mat (rect j e t) := by
…

    Mentions: OAI.PowerSaving.Cluster.J, OAI.PowerSaving.Cluster.H, OAI.PowerSaving.Cluster.rect

  51. lemma OAI.PowerSaving.Cluster.singleton_proj line 199
  52. lemma OAI.PowerSaving.Cluster.big_proj line 204
  53. lemma OAI.PowerSaving.Cluster.belt_proj line 208
  54. lemma OAI.PowerSaving.Cluster.ystart_proj line 214
  55. lemma OAI.PowerSaving.Cluster.xstep_proj line 225
  56. lemma OAI.PowerSaving.Cluster.ystep_proj line 235