OAI/Analysis/FourierLLogL/Edges/Charge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Wire.toll line 15
2. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.mark_total line 19
3. theorem OAI.FourierLLogL.Dyadic.Procedure.Wire.edge_total line 84

   Source documentation

   All length charge or the version using trailing K.

   theorem edge_total (p : Policy M) (main : Bool) (t : Wire M s) {a : Bool}
       (h : Valid t a) (hm : 0 < s.mass) (K : ℕ) (hk : ∀ x : Scene M, K=0 ∨ reach (p x) ≤ K) :
       t.expenditure (toll p main) ≤ 128*t.expenditure (due K)+2*K := by
   …

   Mentions: OAI.FourierLLogL.Dyadic.Procedure.Wire.Policy, OAI.FourierLLogL.Dyadic.Procedure.Wire, OAI.FourierLLogL.Dyadic.Procedure.Wire.Valid, OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.reach, OAI.FourierLLogL.Dyadic.Procedure.Wire.toll, OAI.FourierLLogL.Dyadic.Procedure.Wire.due