OAI/Analysis/FourierLLogL/Assembly/Tokens.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.lowI line 19
  2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.highI line 20
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.playsL line 21
  4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.picks line 22
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.priciest line 25
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.mutedR line 27
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.pricey line 31

    Source documentation

    scalar edge charges pay the largest bad level, chosen locally at the pre-bit moment.

    lemma pricey (s : Scene M) (j : ℕ) (b : Bool) (i : ℕ) (h : picks s i j b) :
    side i ≤ 128*mutedR s j b := by
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.picks, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.mutedR

  8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.special line 43
  9. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.token line 45
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.token_floor line 50
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.tokens_nonneg line 66
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.amp_test line 69
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.side_ant line 84
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.direct_point line 89

    Source documentation

    Each unmasked direct jump outside the main intervals can be paid by its amplitude-selected coupons. During the recursion node n hasn't entered or is unmasked for its scalar level.

    lemma direct_point {s : Scene M} {L : Path M} {x u : Grid M} (h : Trip x s L)
    (j : ℕ) (c : Bool) (a : Grade → ℕ) (hh : shades a u L j)
    (n : ℕ) (l r : Path M) (b : Beat M)
    (hR : c=true → stall u (tagM (mainIx j)) j L l)
    (hc : ∀ i ∈ Finset.Ico (lowI j c) n, stall u (tagL i) j L l)
    (_hn : n ∈ Set.Icc (lowI j c) (highI j M c)) (hl : L=l++r)
    (hm : b∈l) (hb : n < highI j M c → 4*side n < ampU b.post u) :
    ‖proceeds x u b‖ ≤ token a L j c b := by
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Paths.Path, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Paths.Trip, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.Grade, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.shades, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stall, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.tagM, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.lowI, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.tagL, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.highI, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.ampU, OAI.FourierLLogL.Dyadic.Procedure.Paths.proceeds, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.token

  15. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.tokenCost line 176
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.cross_subtotal line 181
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.max_tokens line 188