OAI/Analysis/FourierLLogL/Edges/Intervals.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Charging marked intervals on the path

  1. abbrev OAI.FourierLLogL.Dyadic.Procedure.Wire.Policy line 16
  2. def OAI.FourierLLogL.Dyadic.Procedure.Wire.tags line 18
  3. def OAI.FourierLLogL.Dyadic.Procedure.Wire.labels line 20
  4. def OAI.FourierLLogL.Dyadic.Procedure.Wire.due line 25

    Source documentation

    index budget K=0 requests the all-bit bound

    def due (K : ℕ) (e : Pulse M) : ℝ :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Pulse

  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.due_nonneg line 28
  6. def OAI.FourierLLogL.Dyadic.Procedure.Wire.fading line 31
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.faded line 35
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.fades line 45
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.mark_rent line 53
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.fades_suffix line 105
  11. theorem OAI.FourierLLogL.Dyadic.Procedure.Wire.mark_intervals line 127