OAI/Analysis/FourierLLogL/Capture/Curve.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Adaptive frequency list along a plateau

  1. def OAI.FourierLLogL.Dyadic.Procedure.Capture.speed line 16
  2. def OAI.FourierLLogL.Dyadic.Procedure.Capture.horizon line 17
  3. def OAI.FourierLLogL.Dyadic.Procedure.Capture.localSize line 18
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.speed_pos line 21
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.speed_le line 22
  6. structure OAI.FourierLLogL.Dyadic.Procedure.Capture.Widen line 28

    Source documentation

    One or several appends before a jump.

    structure Widen (p : Scene M) (i : ℕ) (main : Bool) (c d : Chart M) : Prop where
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Capture.Chart

  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.widen_done line 37
  8. def OAI.FourierLLogL.Dyadic.Procedure.Capture.zoom line 67
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.zoom_spec line 70
  10. def OAI.FourierLLogL.Dyadic.Procedure.Capture.goal line 84
  11. def OAI.FourierLLogL.Dyadic.Procedure.Capture.buildup line 88
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.buildup_ran line 91
  13. def OAI.FourierLLogL.Dyadic.Procedure.Capture.chartDebt line 95
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.buildup_total line 98