OAI/Computability/FourierTransform/NetworkStages.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PowerSaving.Cluster.Key line 9
2. abbrev OAI.PowerSaving.Cluster.Other line 10
3. abbrev OAI.PowerSaving.Cluster.Across line 11
4. abbrev OAI.PowerSaving.Cluster.AllAux line 12
5. def OAI.PowerSaving.Cluster.nrRoles line 14
6. def OAI.PowerSaving.Cluster.tower line 15
7. def OAI.PowerSaving.Cluster.mcol line 16
8. def OAI.PowerSaving.Cluster.bankSave line 17
9. abbrev OAI.PowerSaving.Cluster.Spare line 19
10. abbrev OAI.PowerSaving.Cluster.Role line 20
11. instance OAI.PowerSaving.Cluster.keyDec line 21
12. instance OAI.PowerSaving.Cluster.otherDec line 22
13. instance OAI.PowerSaving.Cluster.auxDec line 23
14. instance OAI.PowerSaving.Cluster.roleDec line 24
15. instance OAI.PowerSaving.Cluster.keyType line 25
16. instance OAI.PowerSaving.Cluster.otherType line 26
17. instance OAI.PowerSaving.Cluster.auxType line 27
18. instance OAI.PowerSaving.Cluster.roleType line 28
19. abbrev OAI.PowerSaving.Cluster.gx line 30
20. abbrev OAI.PowerSaving.Cluster.gy line 31
21. abbrev OAI.PowerSaving.Cluster.gu line 32
22. lemma OAI.PowerSaving.Cluster.card_key line 34
23. lemma OAI.PowerSaving.Cluster.card_other line 37
24. lemma OAI.PowerSaving.Cluster.card_aux line 43
25. lemma OAI.PowerSaving.Cluster.card_block line 47
26. lemma OAI.PowerSaving.Cluster.card_allAux line 48
27. lemma OAI.PowerSaving.Cluster.card_role line 53
28. def OAI.PowerSaving.Cluster.locate line 58
29. def OAI.PowerSaving.Cluster.omitJ line 61
30. lemma OAI.PowerSaving.Cluster.locate_self line 62
31. lemma OAI.PowerSaving.Cluster.omit_locate line 64
32. lemma OAI.PowerSaving.Cluster.locate_omit line 66
33. lemma OAI.PowerSaving.Cluster.loc_inj line 68
34. def OAI.PowerSaving.Cluster.world line 74
35. lemma OAI.PowerSaving.Cluster.world_inj line 79
36. def OAI.PowerSaving.Cluster.position line 86
37. lemma OAI.PowerSaving.Cluster.pos_dis line 89
38. lemma OAI.PowerSaving.Cluster.pos_x line 95
39. lemma OAI.PowerSaving.Cluster.pos_y line 98
40. lemma OAI.PowerSaving.Cluster.pos_aux line 101
41. def OAI.PowerSaving.Cluster.axes line 105

    Source documentation

    Global basis and its restriction.

    def axes (j : J) (d : Other j) : StartAxes := fun i =>
    …

    Mentions: OAI.PowerSaving.Cluster.J, OAI.PowerSaving.Cluster.Other, OAI.PowerSaving.Cluster.StartAxes

42. def OAI.PowerSaving.Cluster.bases line 108
43. lemma OAI.PowerSaving.Cluster.bases_local line 113
44. def OAI.PowerSaving.Cluster.region line 125

    Source comment

    Border X has t free axes; Y the same mask with zero address removed.

    def region (t : ℕ) : Mask := univ.filter fun x => ∀ i:J, t ≤ i.val → x i=0

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

45. def OAI.PowerSaving.Cluster.pole line 126
46. def OAI.PowerSaving.Cluster.rim line 127
47. def OAI.PowerSaving.Cluster.border line 128
48. lemma OAI.PowerSaving.Cluster.in_reg line 134
49. lemma OAI.PowerSaving.Cluster.region_begin line 136
50. lemma OAI.PowerSaving.Cluster.region_end line 145
51. lemma OAI.PowerSaving.Cluster.rim_begin line 148
52. lemma OAI.PowerSaving.Cluster.rim_end line 160
53. lemma OAI.PowerSaving.Cluster.border_bp line 178
54. lemma OAI.PowerSaving.Cluster.border_end line 188
55. def OAI.PowerSaving.Cluster.stageOp line 201
56. def OAI.PowerSaving.Cluster.stageLoss line 206
57. lemma OAI.PowerSaving.Cluster.stage line 208