OAI/Analysis/FourierLLogL/Assembly/Gross.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.jackpot line 19
  2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.annual line 21
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.fit_ticket line 28
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.annual_valid line 35
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.normStamp line 66

    Source documentation

    Prices in true history.

    def normStamp (s : Scene M) (j : ℕ) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene

  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.billOf line 68
  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.netGross line 73
  8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.yieldA line 74
  9. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.overdue line 76
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.dueEmpty line 79
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.due_restart line 82
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.cost_jump line 84
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.cost_attempt line 124
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.cost_overall line 136