OAI/Analysis/FourierLLogL/Paths/Wager.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. structure OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk line 19

    Source documentation

    A predictable linear wager driven by the revealed output bit, with quadratic cost.

    structure Desk (M : ℕ) (E : Type*) where
…
  2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.single line 25
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.pay line 26
  4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.tally line 28
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.peak line 32
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.peak_base line 36
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.peak_on line 44
  8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.heatW line 51
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.heatW_one line 54
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.edge_score line 56
  11. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.purses line 60
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.purses_high line 61
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.single_mean line 72
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.peak_mean line 80
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Desk.heat_bound line 102