OAI/Analysis/FourierLLogL/Compress/Cost.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Compress.tot line 18
2. def OAI.FourierLLogL.Compress.ans line 20
3. def OAI.FourierLLogL.Compress.bill line 24

   Source documentation

   Noisy bill: cross entropy with fixed comparator law per position, entropy of letter vector conditional on noisy sum, plus error cost.

   def bill (tag : α → G) (c : G → ℝ) (q : Law α)
       (P : Law Ω) (X : Ω → ι → α) (U : Ω → G) :=
   …

   Mentions: OAI.FourierLLogL.Law

4. lemma OAI.FourierLLogL.Compress.bill_send line 28
5. lemma OAI.FourierLLogL.Compress.bill_mixture_le line 33
6. lemma OAI.FourierLLogL.Compress.bill_cont line 42
7. lemma OAI.FourierLLogL.Compress.bill_through_le line 48
8. def OAI.FourierLLogL.Compress.covered line 56

   Source documentation

   All letters have support contained in comparison law's.

   def covered (P : Law Ω) (X : Ω → ι → α) (q : Law α) : Prop :=
   …

   Mentions: OAI.FourierLLogL.Law

9. lemma OAI.FourierLLogL.Compress.covered_pack line 59
10. lemma OAI.FourierLLogL.Compress.sum_crosspack line 65
11. lemma OAI.FourierLLogL.Compress.kl_le_bill line 70
12. lemma OAI.FourierLLogL.Compress.bill_nonneg line 77
13. lemma OAI.FourierLLogL.Compress.bill_with_entropy line 83
14. lemma OAI.FourierLLogL.Compress.bill_change line 100
15. lemma OAI.FourierLLogL.Compress.bill_condition line 118
16. lemma OAI.FourierLLogL.Compress.sum_split' line 142
17. def OAI.FourierLLogL.Compress.keep line 149
18. lemma OAI.FourierLLogL.Compress.bill_split line 151
19. lemma OAI.FourierLLogL.Compress.bill_subfamily line 203
20. lemma OAI.FourierLLogL.Compress.covered_subfamily line 222
21. lemma OAI.FourierLLogL.Compress.covered_after line 226