OAI/Analysis/FourierLLogL/Procedure/Deficit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Conditional entropy on a fork with a fixed input signal

  1. def OAI.FourierLLogL.Dyadic.Procedure.levels line 18

    Source documentation

    Remaining number of bits in nats

    def levels (s : Scene M) := ((M-s.here.lev:ℕ):ℝ)*log 2

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene

  2. def OAI.FourierLLogL.Dyadic.Procedure.deficit line 19
  3. def OAI.FourierLLogL.Dyadic.Procedure.sideH line 21
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.cap_entropy line 25
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.deficit_nonneg line 33
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.levels_child line 37
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.conditioned_balance line 45
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.old_entropy_cost line 60
  9. def OAI.FourierLLogL.Dyadic.Procedure.hist line 70

    Source documentation

    Observation mass relative to s.norm.

    def hist (s : Scene M) (k : Grid M → Law α) (i : α) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Law

  10. def OAI.FourierLLogL.Dyadic.Procedure.diff line 72
  11. def OAI.FourierLLogL.Dyadic.Procedure.fisher line 75
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.hist_special line 78
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.hist_source line 81
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.bit_cost line 88
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.bit_def line 100
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.space_deficit line 147
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.member_deficit line 161