OAI/Analysis/FourierLLogL/Paths/Screen.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.depthB line 19
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.depth_next line 21
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.muted line 25
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.mute_cat line 29
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.first_on line 37
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.close_persists line 49
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.reach_persists line 59
  8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.snag line 66

    Source documentation

    snag only denotes a nonbad high depth.

    def snag (g : Grade) (x : Grid M) (b : Beat M) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.Grade, OAI.FourierLLogL.Dyadic.Grid

  9. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.ink line 69
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.mute_distance line 71
  11. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.volumeAt line 94
  12. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.betweenS line 97
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.screen_time line 100
  14. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stall line 159
  15. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.billWait line 161
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.bound_stage line 163