OAI/Analysis/FourierLLogL/Compress/Context.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.FourierLLogL.Compress.Labelled line 17

    Source documentation

    Numerical Context State.

    structure Labelled (A : Type) [Fintype A] where
…
  2. def OAI.FourierLLogL.Compress.initial line 24
  3. def OAI.FourierLLogL.Compress.refines line 26
  4. lemma OAI.FourierLLogL.Compress.refines_refl line 29
  5. lemma OAI.FourierLLogL.Compress.refines_trans line 32
  6. def OAI.FourierLLogL.Compress.lblSum line 38
  7. def OAI.FourierLLogL.Compress.lblCtx line 40
  8. def OAI.FourierLLogL.Compress.lblP line 44

    Source documentation

    m-letter block of joint letter-and-context pairs, iid.

    def lblP (W : Labelled A) (m : ℕ) := iid W.law m

    Mentions: OAI.FourierLLogL.Compress.Labelled, OAI.FourierLLogL.Compress.iid

  9. def OAI.FourierLLogL.Compress.fundG line 47

    Source documentation

    Conditional entropy of total sum.

    def fundG (tag : A → G) (p : Labelled A) (m : ℕ) :=
…

    Mentions: OAI.FourierLLogL.Compress.Labelled

  10. def OAI.FourierLLogL.Compress.fundI line 51

    Source documentation

    Conditional exact cost.

    def fundI (tag : A → G) (P : Labelled A) (r : ℕ) :=
…

    Mentions: OAI.FourierLLogL.Compress.Labelled

  11. def OAI.FourierLLogL.Compress.fundK line 55

    Source documentation

    Conditional m-block noisy cost.

    def fundK (tag : A → G) (c : G → ℝ) (P : Labelled A) (m r : ℕ) :=
…

    Mentions: OAI.FourierLLogL.Compress.Labelled

  12. lemma OAI.FourierLLogL.Compress.I_anti line 58
  13. lemma OAI.FourierLLogL.Compress.K_anti line 66
  14. lemma OAI.FourierLLogL.Compress.G_anti line 78
  15. lemma OAI.FourierLLogL.Compress.fundG_one line 93
  16. def OAI.FourierLLogL.Compress.appendOne line 107
  17. lemma OAI.FourierLLogL.Compress.iid_succ line 109
  18. lemma OAI.FourierLLogL.Compress.cons_part line 121
  19. lemma OAI.FourierLLogL.Compress.Hcond_tensor line 129
  20. lemma OAI.FourierLLogL.Compress.Hcond_tensor_right line 138
  21. lemma OAI.FourierLLogL.Compress.lbl_succ_sum line 150
  22. lemma OAI.FourierLLogL.Compress.lbl_succ_ctx line 155
  23. lemma OAI.FourierLLogL.Compress.fundG_succ line 161
  24. lemma OAI.FourierLLogL.Compress.fundG_mono line 174
  25. lemma OAI.FourierLLogL.Compress.opt_succ line 200
  26. lemma OAI.FourierLLogL.Compress.fundI_mono line 254