OAI/Computability/FourierTransform/PrefixTraversal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Prefix computation and tensor gather.

  1. def OAI.PowerSaving.Grove.climb line 12

    Source documentation

    Run state updates in order, with natural prefix addressing. For step: parameters (axis, old prefix, extension digit, previous state).

    def climb {α : Type*} (r : Axes) (x : α)
    (step : ℕ → ℕ → ℕ → α → α) : ℕ → ℕ → α
  | 0 => fun _ => x
  | l+1 => fun i => step l (i/r l) (i%r l) (climb r x step l (i/r l))

    Mentions: OAI.PowerSaving.Grove.Axes

  2. def OAI.PowerSaving.Grove.survey line 17
  3. lemma OAI.PowerSaving.Grove.survey_lt line 20
  4. lemma OAI.PowerSaving.Grove.canopy_survey line 30
  5. theorem OAI.PowerSaving.Grove.graft_survey line 58