OAI/Analysis/FourierLLogL/Paths/Upkeep.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.caveat line 20

    Source documentation

    A local bit-Fisher budget

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

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene

  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.caveat_pos line 23
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.caveat_step line 32
  4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.stats line 95

    Source documentation

    average of forward statistics under uniform output path

    def stats {s : Scene M} (t : Thread M s) (L : Path M → ℝ) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Thread, OAI.FourierLLogL.Dyadic.Procedure.Paths.Path

  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.stats_cons line 98
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.stat_pay line 103
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.stats_nil line 105
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.stats_plus line 106
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.stats_fix line 109
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.caveat_total line 112
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.showers_total line 131
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.flag_point line 159
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.flag_total line 173
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.sum_budget_run line 188