OAI/Analysis/FourierLLogL/Plateau/Local.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Local costs and projected edge bounds

  1. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.debt_at line 14
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.debt_total line 36
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.segment_cost line 56
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.side_deficit line 79
  5. def OAI.FourierLLogL.Dyadic.Procedure.Thread.killed line 122
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.deaths line 125

    Source documentation

    Averaging future removals along uniform output paths, not actual input-choice paths.

    lemma deaths (t : Thread M s) (h : Following j J f t) (hr : 0 < s.norm) :
    t.fee killed ≤ s.mass/s.norm := by
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Thread, OAI.FourierLLogL.Dyadic.Procedure.Thread.Following, OAI.FourierLLogL.Dyadic.Procedure.Thread.killed