OAI/Computability/FourierTransform/LayerCompilation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PowerSaving.RAM.Bench.restricted line 14
  2. def OAI.PowerSaving.RAM.Bench.Study line 18

    Source documentation

    Branches tested by integer registers.

    def Study (b : Bench m ι) (P : ι→Prop) : Prop :=
…

    Mentions: OAI.PowerSaving.RAM.Bench

  3. lemma OAI.PowerSaving.RAM.Bench.Study.transport line 25
  4. lemma OAI.PowerSaving.RAM.Bench.Study.equiv line 30
  5. lemma OAI.PowerSaving.RAM.Bench.Study.lt line 35
  6. lemma OAI.PowerSaving.RAM.Bench.Study.neg line 39
  7. lemma OAI.PowerSaving.RAM.Bench.Study.le line 45
  8. lemma OAI.PowerSaving.RAM.Bench.Study.both line 49
  9. lemma OAI.PowerSaving.RAM.Bench.Study.eq line 56
  10. theorem OAI.PowerSaving.RAM.Bench.chooseM line 62
  11. theorem OAI.PowerSaving.RAM.Bench.branchM line 73
  12. theorem OAI.PowerSaving.RAM.Bench.splice line 81
  13. lemma OAI.PowerSaving.RAM.Bench.chooseN line 92
  14. lemma OAI.PowerSaving.RAM.Bench.branchN line 97
  15. lemma OAI.PowerSaving.RAM.Bench.iteN line 105