OAI/Analysis/FourierLLogL/Compress/Prefix.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Compress.rateH line 13
2. lemma OAI.FourierLLogL.Compress.rate_lt line 16
3. lemma OAI.FourierLLogL.Compress.H_prefix line 20
4. lemma OAI.FourierLLogL.Compress.H_post_prefix line 31
5. abbrev OAI.FourierLLogL.Compress.S line 47
6. lemma OAI.FourierLLogL.Compress.conditional_block_exch line 49
7. lemma OAI.FourierLLogL.Compress.conditional_block_marg line 60
8. lemma OAI.FourierLLogL.Compress.rate_antitone_succ line 71
9. lemma OAI.FourierLLogL.Compress.rate_antitone line 89
10. lemma OAI.FourierLLogL.Compress.rate_bdd line 100
11. lemma OAI.FourierLLogL.Compress.avg_block_kl line 110

    Source documentation

    The joint divergence of the conditional block from the product of its row marginals.

    lemma avg_block_kl {P : Law (S n α G)} (hp : exch P)
        {j m} (hh : j+m ≤ n) (hj : j<n) :
        let X : S n α G → Letters n α := Prod.fst
    …

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Compress.S, OAI.FourierLLogL.Compress.exch, OAI.FourierLLogL.Compress.Letters

12. lemma OAI.FourierLLogL.Compress.kl_uniform line 144
13. lemma OAI.FourierLLogL.Compress.sum_deficit line 159