OAI/Analysis/FourierLLogL/Plateau/Output.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Thread.other line 13
2. def OAI.FourierLLogL.Dyadic.Procedure.Thread.keep line 14
3. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.keep_here line 18
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.other_ok line 20
5. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.keep_true line 23
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.kept_mass line 51

   Source documentation

   law before membership pays q proportionally

   lemma kept_mass (h : Less s q) (hs : ReadyAt s) (ht : ReadyAt q) (hm : 0 < s.mass) :
       q.mass = (keep s q).snip.probs true*s.mass := by
   …

   Mentions: OAI.FourierLLogL.Dyadic.Procedure.Less, OAI.FourierLLogL.Dyadic.Procedure.Thread.keep

7. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.pre_pos line 58
8. def OAI.FourierLLogL.Dyadic.Procedure.Thread.splice line 62
9. def OAI.FourierLLogL.Dyadic.Procedure.Thread.unfoldW line 67
10. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.splice_valid line 72
11. def OAI.FourierLLogL.Dyadic.Procedure.Thread.massLift line 87

    Source documentation

    massLift true-recursion accumulator pays post costs selected at Jump nodes

    def massLift {s : Scene M} (t : Thread M s) (f : Scene M → Scene M → ℝ) : ℝ := match t with
    …

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Thread

12. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.die_average line 92
13. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.output_split line 95
14. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.output_rule line 103
15. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.spliced_cost line 121
16. lemma OAI.FourierLLogL.Dyadic.Procedure.Thread.surcharge_wire line 162