OAI/Analysis/FourierLLogL/Assembly/Cast.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.tailE line 19
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.lone line 23
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.tail_move line 32
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.tail_attempt line 43
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.tail_fail line 59
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.FinJump_align line 84
  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.ordinary line 117

    Source documentation

    Payment from the already open plateau, without its children plateaus.

    def ordinary (u x : Grid M) (t : Play j M s) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Play

  8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.summons line 120
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.ordinary_jump line 127
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.stage_shift line 138

    Source documentation

    common bit selection is correct for the shifted Haar step

    lemma stage_shift (s : Scene M) (t : Play j M s) (u x : Grid M)
    (h : t.Follows J f) (hp : x∈ s.here.block M)
    (hh : finGood (cutoff j) J f x) : tailE s J x u=ordinary u x t+summons u x t := by
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Play, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.finGood, OAI.FourierLLogL.Dyadic.Procedure.cutoff, OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.tailE, OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.ordinary, OAI.FourierLLogL.Dyadic.Procedure.Paths.CastShow.summons