OAI/Analysis/FourierLLogL/Paths/Run.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. structure OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak line 20
  2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.b line 25
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.thick line 26
  4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.rogue line 27
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.every line 28
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.outer line 30
  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.innerV line 31
  8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.flag line 32
  9. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.flagged line 33
  10. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.showers line 34
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.rate line 36
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.thick_rate line 37
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.flag_nonneg line 40
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.flagged_pos line 41
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.showers_pos line 43
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.inner_outer line 45
  17. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.rain line 48
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.cave line 52
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.cave_whole line 90
  20. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.aimed line 112
  21. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.lit_upper line 113
  22. inductive OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.Tray line 135
  23. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.dealer line 141
  24. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.beamRent line 151
  25. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.rent_nonneg line 154
  26. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.rent_total line 158
  27. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.light_bill line 170