OAI/Analysis/FourierLLogL/Edges/Extended.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Full extensions and their bill

  1. def OAI.FourierLLogL.Dyadic.Procedure.Wire.extra line 15

    Source documentation

    Additional unlabelled steps after exit, continuing with a piece frozen.

    def extra (s : Scene M) : ℕ → Wire M s
  | 0 => term s
  | n+1 => link s false fun b => extra (s.smaller b) n

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

  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.extra_ok line 19
  3. def OAI.FourierLLogL.Dyadic.Procedure.Wire.spotDebt line 31

    Source documentation

    Total entropy cost of non-spatial branching.

    def spotDebt {s : Scene M} (t : Wire M s) : ℝ := match t with
…

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

  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.extraDebt line 38
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.due_all line 43
  6. def OAI.FourierLLogL.Dyadic.Procedure.Wire.Turn.up line 100
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.fork_up line 101
  8. def OAI.FourierLLogL.Dyadic.Procedure.Wire.tape line 104

    Source documentation

    Every input experiment extended to full spatial resolution

    def tape {s : Scene M} (t : Road j M s) : Wire M s := match t with
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Road, OAI.FourierLLogL.Dyadic.Procedure.Wire

  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.tape_ok line 112
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.debt_like line 126
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.extra_bill line 150
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.active_charge line 165