OAI/Analysis/FourierLLogL/Finite/Entropy.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Finite conditional entropy

  1. def OAI.FourierLLogL.Law.crossE line 17

    Source documentation

    cross entropy (only meaningful for comparison positive on support).

    def crossE (P : Law α) (q : α → ℝ) : ℝ := P.Ex fun x => -log (q x)

    Mentions: OAI.FourierLLogL.Law

  2. def OAI.FourierLLogL.Law.entropy line 19
  3. lemma OAI.FourierLLogL.Law.entropy_formula line 21
  4. lemma OAI.FourierLLogL.Law.entropy_nonneg line 24
  5. def OAI.FourierLLogL.Law.dominated line 29

    Source documentation

    Positivity on support condition.

    def dominated (P Q : Law α) : Prop := ∀ x, 0 < P x → 0 < Q x

    Mentions: OAI.FourierLLogL.Law

  6. lemma OAI.FourierLLogL.Law.dominated_refl line 31
  7. lemma OAI.FourierLLogL.Law.dominated_send line 33
  8. def OAI.FourierLLogL.Law.kl line 39
  9. lemma OAI.FourierLLogL.Law.entropy_le_cross_aux line 41
  10. lemma OAI.FourierLLogL.Law.kl_nonneg line 57
  11. lemma OAI.FourierLLogL.Law.entropy_uniform line 60
  12. lemma OAI.FourierLLogL.Law.entropy_le_log_card line 65
  13. lemma OAI.FourierLLogL.Law.entropy_point line 75
  14. def OAI.FourierLLogL.Law.H line 80

    Source documentation

    Shannon entropy of an observable on the finite law P.

    def H (P : Law α) (X : α → β) : ℝ := (P.send X).entropy

    Mentions: OAI.FourierLLogL.Law, OAI.FourierLLogL.Law.entropy

  15. def OAI.FourierLLogL.Law.Hcond line 83

    Source documentation

    Conditional entropy H(X|W).

    def Hcond (P : Law α) (X : α → β) (W : α → γ) : ℝ :=
…

    Mentions: OAI.FourierLLogL.Law

  16. lemma OAI.FourierLLogL.Law.H_self line 86
  17. lemma OAI.FourierLLogL.Law.H_nonneg line 88
  18. lemma OAI.FourierLLogL.Law.H_card line 90
  19. lemma OAI.FourierLLogL.Law.H_log line 93
  20. lemma OAI.FourierLLogL.Law.H_congr_mem line 96
  21. lemma OAI.FourierLLogL.Law.H_send line 99
  22. lemma OAI.FourierLLogL.Law.H_partition line 103

    Source documentation

    If two observables induce the same partition, their entropies coincide.

    lemma H_partition (P : Law α) {X : α → β} {Y : α → γ}
    (h : ∀ x y, X x = X y ↔ Y x = Y y) : P.H X = P.H Y := by
…

    Mentions: OAI.FourierLLogL.Law

  23. lemma OAI.FourierLLogL.Law.H_pair_rev line 111
  24. lemma OAI.FourierLLogL.Law.H_constant line 115
  25. lemma OAI.FourierLLogL.Law.Hcond_constant line 121
  26. lemma OAI.FourierLLogL.Law.Hcond_send line 126
  27. lemma OAI.FourierLLogL.Law.H_pair_chain line 130
  28. lemma OAI.FourierLLogL.Law.Hcond_log line 133
  29. lemma OAI.FourierLLogL.Law.Hcond_after line 144
  30. lemma OAI.FourierLLogL.Law.Hcond_nonneg line 150
  31. lemma OAI.FourierLLogL.Law.Hcond_determined line 155
  32. lemma OAI.FourierLLogL.Law.H_le_of_determined line 159
  33. lemma OAI.FourierLLogL.Law.Hcond_le_H line 165
  34. lemma OAI.FourierLLogL.Law.H_associate line 183
  35. lemma OAI.FourierLLogL.Law.Hcond_chain line 187
  36. lemma OAI.FourierLLogL.Law.Hcond_after_cond line 193
  37. lemma OAI.FourierLLogL.Law.Hcond_refine line 204

    Source documentation

    Conditioning reduces entropy.

    lemma Hcond_refine (P : Law α) (X : α → β) (Y : α → γ) (Z : α → η) :
    P.Hcond X (fun x => (Y x,Z x)) ≤ P.Hcond X Z := by
…

    Mentions: OAI.FourierLLogL.Law

  38. lemma OAI.FourierLLogL.Law.Hcond_right_partition line 209
  39. lemma OAI.FourierLLogL.Law.Hcond_antitone line 217
  40. lemma OAI.FourierLLogL.Law.Hcond_subadd line 222
  41. lemma OAI.FourierLLogL.Law.entropy_withNext line 229
  42. lemma OAI.FourierLLogL.Law.entropy_tensorP line 235
  43. lemma OAI.FourierLLogL.Law.H_tensorP line 239