OAI/Computability/FourierTransform/ScalarPreparation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PowerSaving.RAM.Bench.Arch line 15

    Source documentation

    exponent with both it and the power of two available in polynomial resources.

    structure Arch (b : Bench m ι) (e : ι→ℕ) : Prop where
…

    Mentions: OAI.PowerSaving.RAM.Bench

  2. lemma OAI.PowerSaving.RAM.Bench.Arch.transfer line 20
  3. lemma OAI.PowerSaving.RAM.Bench.Arch.fromSmall line 25
  4. lemma OAI.PowerSaving.RAM.Bench.Arch.below line 28
  5. lemma OAI.PowerSaving.RAM.Bench.Arch.succ line 32
  6. lemma OAI.PowerSaving.RAM.Bench.Arch.sub line 36
  7. lemma OAI.PowerSaving.RAM.Bench.powers_fabric line 44
  8. lemma OAI.PowerSaving.RAM.Bench.print_fold line 48
  9. lemma OAI.PowerSaving.RAM.Bench.print_deal line 59
  10. lemma OAI.PowerSaving.RAM.Bench.print_duo line 70
  11. def OAI.PowerSaving.RAM.Bench.towerNote line 80
  12. lemma OAI.PowerSaving.RAM.Bench.note_change line 82
  13. lemma OAI.PowerSaving.RAM.Bench.pulse_duration line 87
  14. lemma OAI.PowerSaving.RAM.Bench.print_pulse line 91
  15. lemma OAI.PowerSaving.RAM.Bench.print_backPulse line 122