OAI/Analysis/FourierLLogL/Assembly/Slab.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.matrix line 19

    Source documentation

    Depth of a sequence (no missing jumps within plateau)

    def matrix (n : ℕ) : Path M → Prop
| [] => True
| b::l => depthB b=n ∧ matrix (n+1) l

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Paths.Path, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.depthB

  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.matrix_trip line 23
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.matrix_cut line 32
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.slab_on line 59
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.shades line 73

    Source documentation

    quality trip coupons that cover all high nonbad jumps before activation.

    def shades (m : Grade → ℕ) (u : Grid M) (l : Path M) (j : ℕ) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.Grade, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Paths.Path

  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.sheds line 77
  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stripe line 82
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stripe_pos line 85
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stripe_bill line 88
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.trim_cost line 113
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.trip_depth_limit line 121