OAI/Analysis/FourierLLogL/Paths/Chief.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. abbrev OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.Tide line 18
  2. structure OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.Tick line 19
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.idle line 24
  4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.going line 25
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.rightNow line 26
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.events line 32
  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.sumbling line 38
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.sumbling_one line 44
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.spark_mean line 53
  10. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.powerOf line 84
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.checkpoints line 86
  12. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.slackOf line 120
  13. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.breakFare line 122
  14. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.quota line 124
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.slack_nonneg line 126
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.fare_step line 130
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.fare_total line 183
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.expected_bling line 213