OAI/Combinatorics/PerfectMatching/Entropy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingEntropy.entropy line 18

   Also declared: ComparatorChallenges/MatchingEntropy.lean:49 (same declaration text).

2. def OAI.MatchingEntropy.marginalEntropy line 21

   Also declared: ComparatorChallenges/MatchingEntropy.lean:52 (same declaration text).

3. def OAI.MatchingEntropy.maxMatchingEntropy line 23

   Also declared: ComparatorChallenges/MatchingEntropy.lean:54 (same declaration text).

4. theorem OAI.MatchingEntropy.entropy_eq line 29

   Source documentation

   Shannon entropy is the literal sum of negative probability-log-probability terms.

   theorem entropy_eq {ι : Type*} [Fintype ι] (p : ι → ℝ) :
       entropy p = -(∑ i, p i * Real.log (p i)) := by
   …

   Mentions: OAI.MatchingEntropy.entropy

5. theorem OAI.MatchingEntropy.continuous_entropy line 33
6. theorem OAI.MatchingEntropy.entropy_nonneg line 38
7. theorem OAI.MatchingEntropy.entropy_le_log_card line 46

   Source documentation

   The entropy bound used in the counting reduction, including zero probabilities.

   theorem entropy_le_log_card {ι : Type*} [Fintype ι] {p : ι → ℝ}
       (hp : p ∈ probabilitySimplex ι) : entropy p ≤ Real.log (Fintype.card ι) := by
   …

   Mentions: OAI.MatchingEntropy.probabilitySimplex, OAI.MatchingEntropy.entropy

8. theorem OAI.MatchingEntropy.LooplessGraph.coordinate_mem_Icc line 67
9. theorem OAI.MatchingEntropy.LooplessGraph.incident_vertex_sum line 80

   Source documentation

   Counting the two distinct endpoints; parallel identities are never collapsed.

   theorem incident_vertex_sum (G : LooplessGraph V E) (e : E) :
       (∑ v, if G.Incident v e then (1 : ℕ) else 0) = 2 := by
   …

10. theorem OAI.MatchingEntropy.LooplessGraph.matching_incident_sum line 94
11. theorem OAI.MatchingEntropy.LooplessGraph.matching_card_twice line 106
12. theorem OAI.MatchingEntropy.LooplessGraph.matching_card line 119
13. theorem OAI.MatchingEntropy.LooplessGraph.indicator_sum line 124
14. theorem OAI.MatchingEntropy.LooplessGraph.marginal_sum line 130

    Source documentation

    All feasible marginal vectors have mass m, as in the entropy proof.

    theorem marginal_sum (G : LooplessGraph V E) {m : ℕ}
        (hV : Fintype.card V = 2 * m) {y : E → ℝ} (hy : y ∈ G.polytope) :
        ∑ e, y e = (m : ℝ) := by
    …

15. theorem OAI.MatchingEntropy.maxMatchingEntropy_attained line 143

    Source documentation

    The supremum in the definition of H is a genuine attained maximum.

    theorem maxMatchingEntropy_attained (G : LooplessGraph V E) {y : E → ℝ}
        (hy : y ∈ G.polytope) :
        ∃ p ∈ G.feasibleLaws y, entropy p = maxMatchingEntropy G y := by
    …

    Mentions: OAI.MatchingEntropy.entropy, OAI.MatchingEntropy.maxMatchingEntropy

16. theorem OAI.MatchingEntropy.maxMatchingEntropy_nonneg line 152
17. theorem OAI.MatchingEntropy.maxMatchingEntropy_le_log_card line 159
18. theorem OAI.MatchingEntropy.entropy_le_maxMatchingEntropy line 167