OAI/Analysis/FourierLLogL/Procedure/Capital.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Deterministic budget state and caps

  1. def OAI.FourierLLogL.Dyadic.Procedure.capA line 11
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.cap_ok line 12
  3. structure OAI.FourierLLogL.Dyadic.Procedure.Fund line 16
  4. def OAI.FourierLLogL.Dyadic.Procedure.Fund.initial line 24
  5. def OAI.FourierLLogL.Dyadic.Procedure.Fund.advance line 25
  6. def OAI.FourierLLogL.Dyadic.Procedure.Fund.breached line 28
  7. def OAI.FourierLLogL.Dyadic.Procedure.Fund.fuel line 29
  8. structure OAI.FourierLLogL.Dyadic.Procedure.Fund.Ok line 31
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Fund.Ok.restrict line 41
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Fund.track_add line 44
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Fund.envelope_scale line 47
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Fund.fund_est line 54