OAI/Computability/FourierTransform/ChunkCompiler.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PowerSaving.Slant.strand line 9
  2. lemma OAI.PowerSaving.Slant.beat_strand line 13
  3. lemma OAI.PowerSaving.Slant.sound_strand line 21
  4. def OAI.PowerSaving.Slant.summary line 28
  5. lemma OAI.PowerSaving.Slant.reads_summary line 31
  6. lemma OAI.PowerSaving.Slant.spill_strand line 36
  7. def OAI.PowerSaving.Slant.quay line 57

    Source documentation

    geometry, p = count*b.

    def quay (b j : ℕ) : Zone := ⟨j*b,b⟩

    Mentions: OAI.PowerSaving.Slant.Zone

  8. def OAI.PowerSaving.Slant.coast line 58
  9. def OAI.PowerSaving.Slant.jetty line 59
  10. lemma OAI.PowerSaving.Slant.quay_fits line 61
  11. lemma OAI.PowerSaving.Slant.jetty_has line 67
  12. lemma OAI.PowerSaving.Slant.jetty_fits line 73
  13. lemma OAI.PowerSaving.Slant.body_sep line 77
  14. lemma OAI.PowerSaving.Slant.quay_sep line 80
  15. lemma OAI.PowerSaving.Slant.quay_peek line 87
  16. lemma OAI.PowerSaving.Slant.spill_quay line 91
  17. lemma OAI.PowerSaving.Slant.reads_quay line 98
  18. def OAI.PowerSaving.Slant.jet_effect line 108

    Source comment

    extend a jetty effect f (given with whole target indexing)
    def jet_effect (p w b s : ℕ) (f : Line→Line) (x : Line) : Line :=
…

    Mentions: OAI.PowerSaving.Line

  19. lemma OAI.PowerSaving.Slant.spill_jet line 111
  20. lemma OAI.PowerSaving.Slant.reads_jet line 135
  21. lemma OAI.PowerSaving.Slant.sum_mult line 140
  22. lemma OAI.PowerSaving.Slant.summary_jet line 148
  23. def OAI.PowerSaving.Slant.wave line 173

    Source comment

    A piece effect for a target chunk s, intermediary chunk c and source chunk j.
    def wave (p b s c j : ℕ) (h g : Line) : Line → Line :=
…

    Mentions: OAI.PowerSaving.Line

  24. def OAI.PowerSaving.Slant.surf line 177

    Source documentation

    Cross term at (p+i) from updated left half of width p.

    def surf (p : ℕ) (h g : Line) (x : Line) : Line :=
…

    Mentions: OAI.PowerSaving.Line

  25. lemma OAI.PowerSaving.Slant.wave_reads line 180
  26. lemma OAI.PowerSaving.Slant.surf_reads line 184
  27. lemma OAI.PowerSaving.Slant.wave_sum line 189
  28. def OAI.PowerSaving.Slant.riprap line 204
  29. lemma OAI.PowerSaving.Slant.beats_riprap line 207
  30. lemma OAI.PowerSaving.Slant.sound_riprap line 212
  31. lemma OAI.PowerSaving.Slant.spill_riprap line 217