OAI/Analysis/FourierLLogL/Paths/Encore.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.chooseCap line 18
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.choice_bounds line 19
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.heartP line 40
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.booking line 43
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.hush line 66
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.spillScore line 69
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.hush_pos line 72
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.spill_share line 75
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.spill_bound line 90
  10. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.timex line 120
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.timex_scores line 124
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stat_jensen line 143
  13. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.dBase line 155
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.paid_levels line 158