OAI/Analysis/FourierLLogL/Snapshot/Activate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.Comes line 15
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.vacant_comes line 23
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.comes_down line 26
  4. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.catches line 43
  5. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.aligned line 46
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.effort_bounds line 50
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.currently line 78
  8. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.latency line 165
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.waiting line 167