OAI/Analysis/FourierLLogL/Assembly/Duration.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.tagM line 19
  2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.tagL line 20
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.depthRate line 21
  4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.mainRatio line 22
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.mainSticker line 26
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.scalarSticker line 28
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.rate_easy line 32
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.mainRatio_one line 34
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.mainSticker_pos line 43
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.scalarSticker_pos line 46
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.ride line 52

    Source documentation

    Bounding a suffix without bigger main activations.

    lemma ride :
    ∀ᶠ j : ℕ in atTop,
      ∀ M J i : ℕ, ∀ s : Scene M, ∀ f : Grid M → ℝ, ∀ l r m : Path M,
        ∀ (b : Beat M) (x u : Grid M),
          let g := tagM i
…

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

  12. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.guardedV line 156

    Source documentation

    Scalar suffix exact part with mask specified by chosen representative.

    def guardedV (i : ℕ) (v : Grid M) (b : Beat M) := guarded v (side i) b.post

    Mentions: OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Paths.guarded

  13. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.ampU line 158
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.mask_estimate line 161