OAI/Computability/FourierTransform/MeasuredPrograms.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PowerSaving.RAM.Bench.spot_jetty line 15
  2. lemma OAI.PowerSaving.RAM.Bench.spot_quay line 21
  3. lemma OAI.PowerSaving.RAM.Bench.carve_speck line 32

    Source comment

    speck s c j for small
    lemma carve_speck {p s c j : ι→ℕ} (hp : b.Digit p)
    (hs : b.Digit s) (hc : b.Digit c) (hj : b.Digit j)
    (hb : ∀ i, c i<p i) (hb' : ∀ i, j i<p i) (hE : ∀ i,p i+w i ≤ e i) :
    b.Engrave (fun i => p i+w i) (fun i => speck (p i) (w i) (h i) (g i) (s i) (c i) (j i)) := by
…
  4. lemma OAI.PowerSaving.RAM.Bench.carve_sand line 61
  5. lemma OAI.PowerSaving.RAM.Bench.carve_gravel line 77
  6. lemma OAI.PowerSaving.RAM.Bench.carve_reef line 123