OAI/Computability/FourierTransform/IntervalPrograms.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PowerSaving.RAM.Bench.Spots line 14
2. lemma OAI.PowerSaving.RAM.Bench.Spots.transfer line 20
3. lemma OAI.PowerSaving.RAM.Bench.Spots.has line 22
4. lemma OAI.PowerSaving.RAM.Bench.Spots.overlay line 26
5. lemma OAI.PowerSaving.RAM.Bench.Spots.shade line 36
6. lemma OAI.PowerSaving.RAM.Bench.Spots.finds line 49
7. lemma OAI.PowerSaving.RAM.Bench.Spots.snap line 54
8. lemma OAI.PowerSaving.RAM.Bench.Spots.slim line 65
9. lemma OAI.PowerSaving.RAM.Bench.Hue.smallNumeral line 71

   Source comment

   Numeric convenience

   lemma Hue.smallNumeral (b : Bench m ι) (n : ℕ) [Nat.AtLeastTwo n] :
       b.Hue (fun _ => (OfNat.ofNat n:ℂ)) := (Hue.numeral n).congr fun _ => rfl
   …

   Mentions: OAI.PowerSaving.RAM.Bench, OAI.PowerSaving.RAM.Bench.Hue.numeral, OAI.PowerSaving.RAM.Bench.Hue.congr

10. lemma OAI.PowerSaving.RAM.Bench.Spots.hinge line 83
11. lemma OAI.PowerSaving.RAM.Bench.Spots.brick line 88
12. lemma OAI.PowerSaving.RAM.Bench.Spots.spark line 95
13. lemma OAI.PowerSaving.RAM.Bench.Spots.flash line 112
14. lemma OAI.PowerSaving.RAM.Bench.engrave_cameo line 121