OAI/Analysis/FourierLLogL/Procedure/Counts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Expected starts, entropy and attempt counts

  1. def OAI.FourierLLogL.Dyadic.Procedure.Road.flatFee line 16
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.flat_finish line 19
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.flat_push line 22
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.flat_fork line 26
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.total_step line 31
  6. def OAI.FourierLLogL.Dyadic.Procedure.Road.beginFee line 46
  7. def OAI.FourierLLogL.Dyadic.Procedure.Road.headroom line 51
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.headroom_nonneg line 52
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.headroom_up line 55
  10. def OAI.FourierLLogL.Dyadic.Procedure.Road.startup line 65
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.startup_ok line 68
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.ticket_count line 72
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.final_coarse line 163
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.attempt_count line 198