OAI/Computability/FourierTransform/TensorIndexing.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Tensor slot multiplication. Natural-number prefix indexing, most significant radix first.

  1. abbrev OAI.PowerSaving.Grove.Axes line 13
  2. def OAI.PowerSaving.Grove.extent line 16

    Source documentation

    volume of the first j axes

    def extent (r : Axes) : ℕ → ℕ
  | 0 => 1
  | j+1 => extent r j*r j

/-- Hypothesis in uses of a tuple index (omit entirely any singleton axes). -/

    Mentions: OAI.PowerSaving.Grove.Axes

  3. def OAI.PowerSaving.Grove.Splits line 21

    Source documentation

    Hypothesis in uses of a tuple index (omit entirely any singleton axes).

    def Splits (r : Axes) (l : ℕ) := ∀ t<l, 2≤r t
…

    Mentions: OAI.PowerSaving.Grove.Axes

  4. lemma OAI.PowerSaving.Grove.Splits.cut line 26
  5. lemma OAI.PowerSaving.Grove.Splits.here line 30
  6. lemma OAI.PowerSaving.Grove.Splits.extent_pow line 33
  7. lemma OAI.PowerSaving.Grove.Splits.extent_pos line 40
  8. lemma OAI.PowerSaving.Grove.Splits.extent_le line 44
  9. lemma OAI.PowerSaving.Grove.Splits.axes_le line 56
  10. lemma OAI.PowerSaving.Grove.Splits.tree_bound line 60
  11. lemma OAI.PowerSaving.Grove.Splits.div_lt line 72
  12. lemma OAI.PowerSaving.Grove.Splits.mod_lt line 76
  13. lemma OAI.PowerSaving.Grove.Splits.join_lt line 79
  14. lemma OAI.PowerSaving.Grove.joined line 88
  15. lemma OAI.PowerSaving.Grove.chops line 89
  16. lemma OAI.PowerSaving.Grove.chips line 92
  17. abbrev OAI.PowerSaving.Grove.Wood line 97

    Source documentation

    natural-address matrices (only read in extent)

    abbrev Wood := ℕ → ℕ → ℂ
  18. def OAI.PowerSaving.Grove.knot line 99
  19. def OAI.PowerSaving.Grove.graft line 102
  20. def OAI.PowerSaving.Grove.white line 105
  21. def OAI.PowerSaving.Grove.frame line 107
  22. lemma OAI.PowerSaving.Grove.front_graft line 109
  23. lemma OAI.PowerSaving.Grove.graft_knot line 114
  24. lemma OAI.PowerSaving.Grove.graft_white line 121
  25. lemma OAI.PowerSaving.Grove.graft_congr line 124
  26. def OAI.PowerSaving.Grove.canopy line 129
  27. lemma OAI.PowerSaving.Grove.canopy_knot line 133
  28. lemma OAI.PowerSaving.Grove.canopy_white line 157
  29. def OAI.PowerSaving.Grove.leafM line 175

    Source comment

    synchronization for a reel at every axis
    def leafM (u : Stroke) : Wood :=
…

    Mentions: OAI.PowerSaving.Grove.Wood

  30. def OAI.PowerSaving.Grove.leafC line 178
  31. lemma OAI.PowerSaving.Grove.graft_leafM line 183
  32. lemma OAI.PowerSaving.Grove.graft_leafC line 186
  33. def OAI.PowerSaving.Grove.trunk line 192
  34. lemma OAI.PowerSaving.Grove.graft_trunk line 198
  35. def OAI.PowerSaving.Grove.forest line 215
  36. lemma OAI.PowerSaving.Grove.graft_forest line 222
  37. lemma OAI.PowerSaving.Grove.trunk_creates line 240
  38. lemma OAI.PowerSaving.Grove.canopy_congr line 251
  39. theorem OAI.PowerSaving.Grove.forest_completes line 262