OAI/Computability/FourierTransform/Layout.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Dense indexing on logical array shapes.

  1. structure OAI.PowerSaving.Layout line 8
  2. def OAI.PowerSaving.Layout.atFin line 19
  3. theorem OAI.PowerSaving.Layout.loc_atFin line 20
  4. def OAI.PowerSaving.Layout.toIx line 23
  5. def OAI.PowerSaving.Layout.index line 25
  6. def OAI.PowerSaving.Layout.tape line 28
  7. theorem OAI.PowerSaving.Layout.read line 31
  8. theorem OAI.PowerSaving.Layout.verify line 36
  9. def OAI.PowerSaving.Layout.std line 47
  10. theorem OAI.PowerSaving.Layout.card line 50
  11. def OAI.PowerSaving.Layout.comap line 53
  12. theorem OAI.PowerSaving.Layout.tape_comap line 62
  13. def OAI.PowerSaving.Layout.someLayout line 71

    Source documentation

    A layout on any fixed finite indexing type; only used for fixed operations.

    noncomputable def someLayout (α : Type*) [Fintype α] : Layout α :=
…

    Mentions: OAI.PowerSaving.Layout

  14. lemma OAI.PowerSaving.Layout.div_join line 74
  15. lemma OAI.PowerSaving.Layout.mod_join line 77
  16. lemma OAI.PowerSaving.Layout.lt_join line 79
  17. def OAI.PowerSaving.Layout.pair line 85

    Source documentation

    First factor slow, second factor fast.

    def pair (X : Layout α) (Y : Layout β) : Layout (α × β) where
…

    Mentions: OAI.PowerSaving.Layout

  18. lemma OAI.PowerSaving.Layout.pair_len line 106
  19. lemma OAI.PowerSaving.Layout.pair_loc line 109
  20. lemma OAI.PowerSaving.Layout.pair_div line 112
  21. lemma OAI.PowerSaving.Layout.pair_mod line 114
  22. def OAI.PowerSaving.Layout.cat line 118

    Source documentation

    Disjoint coordinate intervals.

    def cat (X : Layout α) (Y : Layout β) : Layout (α ⊕ β) where
…

    Mentions: OAI.PowerSaving.Layout

  23. def OAI.PowerSaving.Layout.expand line 145
  24. lemma OAI.PowerSaving.Layout.expand_zero line 148
  25. lemma OAI.PowerSaving.Layout.expand_succ line 150
  26. lemma OAI.PowerSaving.Layout.expand_lt line 156
  27. lemma OAI.PowerSaving.Layout.expand_entry line 161
  28. lemma OAI.PowerSaving.Layout.expand_onto line 172
  29. def OAI.PowerSaving.Layout.vecFin line 185
  30. def OAI.PowerSaving.Layout.permFn line 197

    Source documentation

    Uniform radix on axes in layout J.

    def permFn (e : α ≃ β) (μ : Type*) : (α → μ) ≃ (β → μ) where
…
  31. def OAI.PowerSaving.Layout.digits line 203
  32. theorem OAI.PowerSaving.Layout.digits_len line 206
  33. theorem OAI.PowerSaving.Layout.digits_code line 209
  34. theorem OAI.PowerSaving.Layout.digits_entry line 217