OAI/Analysis/FourierLLogL/Finite/Mixture.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Entropy of mixtures

  1. lemma OAI.FourierLLogL.Law.send_withNext line 16
  2. lemma OAI.FourierLLogL.Law.H_withNext line 22
  3. lemma OAI.FourierLLogL.Law.Hcond_withNext line 28
  4. lemma OAI.FourierLLogL.Law.Hcond_withNext' line 42
  5. lemma OAI.FourierLLogL.Law.Hcond_through line 49
  6. lemma OAI.FourierLLogL.Law.H_through_ge line 55
  7. lemma OAI.FourierLLogL.Law.H_through_le line 61
  8. def OAI.FourierLLogL.Law.coinP line 67
  9. lemma OAI.FourierLLogL.Law.coinP_Ex line 70
  10. lemma OAI.FourierLLogL.Law.coinP_entropy line 74
  11. lemma OAI.FourierLLogL.Law.mixture_eq_through line 77
  12. lemma OAI.FourierLLogL.Law.H_mixture_ge line 83
  13. lemma OAI.FourierLLogL.Law.Hcond_mixture_ge line 89
  14. lemma OAI.FourierLLogL.Law.entropy_mixture_le line 96
  15. lemma OAI.FourierLLogL.Law.entropy_mixture_ge line 107
  16. lemma OAI.FourierLLogL.Law.entropy_le_log_size line 112

    Source documentation

    Support version of the entropy bound.

    lemma entropy_le_log_size (P : Law α) (s : Finset α)
    (h : ∀ x, 0 < P x → x ∈ s) : P.entropy ≤ log (s.card : ℝ) := by
…

    Mentions: OAI.FourierLLogL.Law

  17. theorem OAI.FourierLLogL.Law.entropy_le_of_tv line 135

    Source documentation

    Entropy modulus sufficient for the replacement by independent letters.

    theorem entropy_le_of_tv (P Q : Law α) (s : Finset α)
    (h : ∀ x, 0 < P x → x ∈ s) :
    P.entropy ≤ Q.entropy + (log 2 + P.tv Q * log (s.card:ℝ)) := by
…

    Mentions: OAI.FourierLLogL.Law