OAI/Computability/FourierTransform/IntervalEffects.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Disjoint interval effects of layer words. In particular a composition of two rectangular maps can be added by a commutator of adds on an arbitrary-content intermediate.

  1. structure OAI.PowerSaving.Slant.Zone line 11
  2. def OAI.PowerSaving.Slant.Zone.has line 16
  3. instance OAI.PowerSaving.Slant.Zone.instDecidableHas line 18
  4. def OAI.PowerSaving.Slant.Zone.Fits line 22
  5. lemma OAI.PowerSaving.Slant.Zone.fits_of line 24
  6. lemma OAI.PowerSaving.Slant.Zone.fits_empty line 27
  7. def OAI.PowerSaving.Slant.Zone.Sep line 30
  8. lemma OAI.PowerSaving.Slant.Zone.sep_of line 32
  9. lemma OAI.PowerSaving.Slant.Zone.Sep.symm line 35
  10. lemma OAI.PowerSaving.Slant.Zone.inside line 37
  11. lemma OAI.PowerSaving.Slant.Zone.enter line 40
  12. lemma OAI.PowerSaving.Slant.Zone.identify line 44
  13. lemma OAI.PowerSaving.Slant.Zone.boundary line 47
  14. def OAI.PowerSaving.Slant.Zone.peek line 51

    Source documentation

    Only read entries within 'wide'; other values are ignored.

    def peek (u : Zone) (x : Line) : Line := drift u.lo x

    Mentions: OAI.PowerSaving.Slant.Zone, OAI.PowerSaving.Line

  15. def OAI.PowerSaving.Slant.Zone.slim line 53
  16. lemma OAI.PowerSaving.Slant.Zone.slim_has line 55
  17. lemma OAI.PowerSaving.Slant.Zone.Fits.slim line 58
  18. lemma OAI.PowerSaving.Slant.Zone.Sep.slim_left line 61
  19. lemma OAI.PowerSaving.Slant.Zone.Sep.slim_right line 64
  20. def OAI.PowerSaving.Slant.Reads line 70

    Source documentation

    f read only first p entries for the first q output entries

    def Reads (p q : ℕ) (f : Line → Line) : Prop :=
…

    Mentions: OAI.PowerSaving.Line

  21. def OAI.PowerSaving.Slant.AdditiveOn line 73
  22. def OAI.PowerSaving.Slant.minusFn line 76
  23. structure OAI.PowerSaving.Slant.Spill line 78
  24. lemma OAI.PowerSaving.Slant.Spill.preserves line 85
  25. lemma OAI.PowerSaving.Slant.Spill.congr line 89
  26. def OAI.PowerSaving.Slant.cameo line 97

    Source documentation

    The commutator construction. Disjoint x->z, z->y adds.

    def cameo (a b c d : Reel) : Reel := ((a.stack b).stack c).stack d

    Mentions: OAI.PowerSaving.Slant.Reel

  27. lemma OAI.PowerSaving.Slant.sound_cameo line 99
  28. theorem OAI.PowerSaving.Slant.spill_cameo line 104