OAI/Analysis/FourierLLogL/Edges/Wire.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Complete spatial wires reading every bit to leaf

  1. def OAI.FourierLLogL.Dyadic.Procedure.Fork.pitch line 18

    Source documentation

    dry, single-bit price

    def pitch (q : Fork M) := log 2 - q.probs.entropy

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Fork

  2. def OAI.FourierLLogL.Dyadic.Procedure.Fork.whistle line 19
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.pitch_nonneg line 21
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.pitch_eq line 24
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.whistle_high line 30
  6. structure OAI.FourierLLogL.Dyadic.Procedure.Pulse line 53
  7. def OAI.FourierLLogL.Dyadic.Procedure.Pulse.signal line 59
  8. def OAI.FourierLLogL.Dyadic.Procedure.Pulse.realized line 60
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Pulse.signal_nonneg line 61
  10. structure OAI.FourierLLogL.Dyadic.Procedure.TossUp line 65

    Source documentation

    Generic membership fork, same spatial node both children.

    structure TossUp (s : Scene M) where
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene

  11. def OAI.FourierLLogL.Dyadic.Procedure.TossUp.snip line 69
  12. inductive OAI.FourierLLogL.Dyadic.Procedure.Wire line 71
  13. inductive OAI.FourierLLogL.Dyadic.Procedure.Wire.Part line 78
  14. def OAI.FourierLLogL.Dyadic.Procedure.Wire.ReadyAt line 81
  15. def OAI.FourierLLogL.Dyadic.Procedure.Wire.Valid line 84

    Source documentation

    valid with active prefix

    def Valid {s : Scene M} (t : Wire M s) (a : Bool) : Prop :=
…

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

  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.Valid.atSrc line 94
  17. def OAI.FourierLLogL.Dyadic.Procedure.Wire.read line 97
  18. def OAI.FourierLLogL.Dyadic.Procedure.Wire.expenditure line 106
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.linkEx line 109
  20. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.spotEx line 116
  21. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.fee_stay line 123
  22. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.fee_spot line 126
  23. lemma OAI.FourierLLogL.Dyadic.Procedure.Wire.fee_link line 131