OAI/Analysis/FourierLLogL/Procedure/Surprisal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Increments in the input model

  1. def OAI.FourierLLogL.Dyadic.Procedure.Event.surprise line 15
  2. def OAI.FourierLLogL.Dyadic.Procedure.Event.failFee line 16
  3. def OAI.FourierLLogL.Dyadic.Procedure.Event.winFee line 19
  4. def OAI.FourierLLogL.Dyadic.Procedure.Event.memFee line 22
  5. def OAI.FourierLLogL.Dyadic.Procedure.Event.count line 23
  6. def OAI.FourierLLogL.Dyadic.Procedure.Event.tried line 26
  7. def OAI.FourierLLogL.Dyadic.Procedure.Event.likelihood line 29
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Event.surprise_nonneg line 33
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Event.fee_bounds line 35
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Event.price_space line 45
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Event.surprisal_cost line 64
  12. def OAI.FourierLLogL.Dyadic.Procedure.Journal.membership line 95
  13. def OAI.FourierLLogL.Dyadic.Procedure.Journal.creditSum line 96
  14. def OAI.FourierLLogL.Dyadic.Procedure.Journal.debit line 97
  15. def OAI.FourierLLogL.Dyadic.Procedure.Journal.like line 98
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Journal.mem_parts line 100
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.Journal.positive_fee line 107
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.Journal.positive_mem line 109
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.final_sound line 116
  20. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.capital_bound line 178

    Source documentation

    Positive exponential fee supported on path prefixes.

    lemma capital_bound {s : Scene M} (F : Event j M → ℝ)
    (hp : ∀ s : Scene M, ∀ v : Pace, F (Event.pace s v)=0)
    (hf : ∀ s : Scene M, ∀ v : Turn j s,
      v.fork.probs.Ex (fun b => exp (F (.march s v b))) ≤ 1)
    (t : Road j M s) {f : Grid M → ℝ} (h : t.Trusted J f) (hm : 0 < s.mass) :
    t.expHike (fun l _x => exp (l.fee F)) ≤ 1 := by
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Event, OAI.FourierLLogL.Dyadic.Procedure.Pace, OAI.FourierLLogL.Dyadic.Procedure.Turn, OAI.FourierLLogL.Dyadic.Procedure.Road, OAI.FourierLLogL.Dyadic.Grid