OAI/Computability/FourierTransform/ParameterPrograms.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Primitive O(n) and O(polylog(n)) algorithms for parameters.

  1. def OAI.PowerSaving.RAM.tallyH line 11

    Source comment

    halving and log. All-natural iterations.
    def tallyH (n : ℕ) : ℕ → ℕ×ℕ
  | 0 => (n,0)
  | k+1 => let p := tallyH n k
…
  2. lemma OAI.PowerSaving.RAM.tallyH.small line 18
  3. lemma OAI.PowerSaving.RAM.tallyH.tally line 23
  4. lemma OAI.PowerSaving.RAM.tallyH.quota line 37
  5. lemma OAI.PowerSaving.RAM.tallyH.end_eq line 43
  6. lemma OAI.PowerSaving.RAM.Bench.Nick.cmp line 53
  7. lemma OAI.PowerSaving.RAM.Bench.Nick.logM line 57
  8. lemma OAI.PowerSaving.RAM.Bench.Nick.numeralM line 73