OAI/Analysis/FourierLLogL/Plateau/Thread.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

A plateau without its restart markers

  1. def OAI.FourierLLogL.Dyadic.Procedure.minimumT line 13
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.minimum_pos line 15
  3. structure OAI.FourierLLogL.Dyadic.Procedure.Less line 17
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.less_self line 24
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Less.trans line 27
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.less_lost line 31
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Less.antitone line 34
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Less.mass_le line 36
  9. def OAI.FourierLLogL.Dyadic.Procedure.shrink line 41
  10. inductive OAI.FourierLLogL.Dyadic.Procedure.Thread line 44
  11. def OAI.FourierLLogL.Dyadic.Procedure.Thread.Following line 49
  12. def OAI.FourierLLogL.Dyadic.Procedure.Thread.reattach line 55
  13. def OAI.FourierLLogL.Dyadic.Procedure.Thread.project line 60
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.rooted line 70
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.projected line 73
  16. structure OAI.FourierLLogL.Dyadic.Procedure.Thread.Beat line 108

    Source documentation

    Local output paths, excluding terminal removals (unnecessary for transform).

    structure Beat (M : ℕ) where
…
  17. def OAI.FourierLLogL.Dyadic.Procedure.Thread.stream line 113
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.step_dice_child line 119
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.stream_branch line 127
  20. def OAI.FourierLLogL.Dyadic.Procedure.Thread.fee line 149
  21. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.fee_ran line 152