OAI/Analysis/FourierLLogL/Snapshot/Rec.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Timing of snapshot replacement and local charges

  1. structure OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Board line 17
  2. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.vacant line 21
  3. structure OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot line 23
  4. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.closer line 28
  5. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.freshAt line 32

    Source documentation

    refresh test. Ignore when breaching the cap.

    def freshAt (a : Plot) (g : Board M) (x : Scene M) : Prop :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot, OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Board, OAI.FourierLLogL.Dyadic.Procedure.Scene

  6. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.now line 38
  7. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.cardStep line 40
  8. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.turn line 42
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.turn_chart line 47
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.prior_step line 50
  11. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.deltaC line 56
  12. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.birth line 62
  13. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.marker line 64
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.marker_pos line 66
  15. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.soundPrev line 69
  16. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.creditsC line 72
  17. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.slotC line 75
  18. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.kObs line 78
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.deltaC_pos line 80
  20. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.costC_pos line 88
  21. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.slot_pos line 90
  22. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.turn_prev line 92
  23. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.changed_point line 99
  24. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.coinC line 219
  25. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.debtC line 221
  26. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.debt_recur line 224
  27. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.expenses line 323
  28. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.expenses_nonneg line 326
  29. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.minted line 344

    Source documentation

    number born before cap breach; representatives from these births may be retained for delayed estimates on further jumps

    def minted (p : Plot) (g : Board M) : List (Beat M) → ℝ
| [] => 0
| b::l => let c := p.turn g b.post
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot, OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Board

  30. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Plot.mint_small line 349