OAI/Combinatorics/CliqueFree/FiniteEntropy.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CliqueFreeIndependence.FiniteEntropy.IsProb line 21

   Source documentation

   A finite real-valued probability vector.

   def IsProb (p : I → ℝ) : Prop := (∀ i, 0 ≤ p i) ∧ ∑ i, p i = 1

2. def OAI.CliqueFreeIndependence.FiniteEntropy.entropy line 24

   Source documentation

   Weighted row entropy, with the 0 log 0 = 0 convention.

   def entropy (w p : I → ℝ) : ℝ := ∑ i, p i * Real.log (w i / p i)

3. def OAI.CliqueFreeIndependence.FiniteEntropy.divergence line 27

   Source documentation

   Relative entropy, used only when q is positive on the positive support of p.

   def divergence (p q : I → ℝ) : ℝ := ∑ i, p i * Real.log (p i / q i)

4. def OAI.CliqueFreeIndependence.FiniteEntropy.tv line 30

   Source documentation

   Total variation distance of two finite probability vectors.

   def tv (p q : I → ℝ) : ℝ := (∑ i, |p i - q i|) / 2

5. lemma OAI.CliqueFreeIndependence.FiniteEntropy.relTerm_nonneg line 32
6. lemma OAI.CliqueFreeIndependence.FiniteEntropy.sqrt_sub_sq_le_relTerm line 47
7. lemma OAI.CliqueFreeIndependence.FiniteEntropy.divergence_nonneg line 70
8. lemma OAI.CliqueFreeIndependence.FiniteEntropy.hellinger_le_divergence line 75
9. lemma OAI.CliqueFreeIndependence.FiniteEntropy.tv_nonneg line 82
10. lemma OAI.CliqueFreeIndependence.FiniteEntropy.tv_sq_le_hellinger line 85
11. lemma OAI.CliqueFreeIndependence.FiniteEntropy.entropy_eq_sum line 115
12. lemma OAI.CliqueFreeIndependence.FiniteEntropy.divergence_eq_sum line 123
13. lemma OAI.CliqueFreeIndependence.FiniteEntropy.entropy_ge_neg_log_of_density line 132
14. lemma OAI.CliqueFreeIndependence.FiniteEntropy.tv_comm line 148
15. lemma OAI.CliqueFreeIndependence.FiniteEntropy.tv_triangle line 151
16. lemma OAI.CliqueFreeIndependence.FiniteEntropy.weighted_sq_le line 155
17. lemma OAI.CliqueFreeIndependence.FiniteEntropy.mix_isProb line 177

    Source documentation

    Mixing finitely many probability vectors.

    lemma mix_isProb {a : J → ℝ} {p : J → I → ℝ} (ha : IsProb a)
        (hp : ∀ j, IsProb (p j)) : IsProb (fun i ↦ ∑ j, a j * p j i) := by
    …

    Mentions: OAI.CliqueFreeIndependence.FiniteEntropy.IsProb

18. lemma OAI.CliqueFreeIndependence.FiniteEntropy.mix_support line 185
19. lemma OAI.CliqueFreeIndependence.FiniteEntropy.entropy_mix_gap line 193

    Source documentation

    The finite entropy-mixture identity for the averaged increment.

    lemma entropy_mix_gap {w : I → ℝ} (hw : ∀ i, 0 < w i)
        {a : J → ℝ} {p : J → I → ℝ} (ha : IsProb a) (hp : ∀ j, IsProb (p j)) :
        entropy w (fun i ↦ ∑ j, a j * p j i) - ∑ j, a j * entropy w (p j) =
          ∑ j, a j * divergence (p j) (fun i ↦ ∑ k, a k * p k i) := by
    …

    Mentions: OAI.CliqueFreeIndependence.FiniteEntropy.IsProb, OAI.CliqueFreeIndependence.FiniteEntropy.entropy, OAI.CliqueFreeIndependence.FiniteEntropy.divergence

20. lemma OAI.CliqueFreeIndependence.FiniteEntropy.average_tv_sq_le_average_divergence line 215
21. lemma OAI.CliqueFreeIndependence.FiniteEntropy.mul_log_div line 229
22. lemma OAI.CliqueFreeIndependence.FiniteEntropy.partial_entropy_le line 236
23. lemma OAI.CliqueFreeIndependence.FiniteEntropy.prob_sum_on line 274
24. lemma OAI.CliqueFreeIndependence.FiniteEntropy.entropy_sum_on line 279
25. lemma OAI.CliqueFreeIndependence.FiniteEntropy.entropy_supported_le_log line 286
26. lemma OAI.CliqueFreeIndependence.FiniteEntropy.entropy_supported_concentration line 293
27. lemma OAI.CliqueFreeIndependence.FiniteEntropy.entropy_tail_term line 330
28. lemma OAI.CliqueFreeIndependence.FiniteEntropy.entropy_tail line 350