OAI/Analysis/FourierLLogL/Finite/Comparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Comparison, data processing and Pinsker

  1. lemma OAI.FourierLLogL.Law.kl_ex line 16
  2. lemma OAI.FourierLLogL.Law.after_dominated line 22
  3. lemma OAI.FourierLLogL.Law.kl_chain line 28
  4. lemma OAI.FourierLLogL.Law.kl_data_processing line 44
  5. def OAI.FourierLLogL.Law.tv line 53
  6. lemma OAI.FourierLLogL.Law.tv_nonneg line 55
  7. lemma OAI.FourierLLogL.Law.tv_comm line 57
  8. lemma OAI.FourierLLogL.Law.tv_common line 59
  9. lemma OAI.FourierLLogL.Law.tv_le_one line 65
  10. lemma OAI.FourierLLogL.Law.tv_data_processing line 70
  11. lemma OAI.FourierLLogL.Law.tv_sq_le_kl line 83

    Source documentation

    Pinsker (only need numerical constant). Use log tangent inequality on square roots.

    lemma tv_sq_le_kl {P Q : Law α} (h : P.dominated Q) :
    (P.tv Q)^2 ≤ P.kl Q := by
…

    Mentions: OAI.FourierLLogL.Law

  12. lemma OAI.FourierLLogL.Law.tv_le_sqrt_kl line 126