OAI/Combinatorics/PerfectMatching/Coupling.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingEntropy.fiberMass line 17

   Source documentation

   Finite pushforward weights.

   def fiberMass {A C : Type*} [Fintype A] [DecidableEq C]
       (p : A → ℝ) (f : A → C) (c : C) : ℝ := ∑ a, if f a = c then p a else 0

2. theorem OAI.MatchingEntropy.fiberMass_nonneg line 20
3. theorem OAI.MatchingEntropy.le_fiberMass_self line 27
4. def OAI.MatchingEntropy.jointLaw line 36

   Source documentation

   The explicit cut-choice coupling. Only equal choices receive mass.

   def jointLaw {A B C : Type*} [Fintype A] [Fintype B] [DecidableEq C]
       (p : A → ℝ) (q : B → ℝ) (f : A → C) (g : B → C) (z : A × B) : ℝ :=
   …

5. theorem OAI.MatchingEntropy.jointLaw_nonneg line 40
6. theorem OAI.MatchingEntropy.jointLaw_first line 48
7. theorem OAI.MatchingEntropy.jointLaw_second line 68
8. theorem OAI.MatchingEntropy.jointLaw_mem_simplex line 88
9. theorem OAI.MatchingEntropy.sum_subtype_supported line 97
10. theorem OAI.MatchingEntropy.compatible_jointLaw_mem_simplex line 107

    Source documentation

    No mass is lost in retaining only compatible pairs.

    theorem compatible_jointLaw_mem_simplex {A B C : Type*} [Fintype A] [Fintype B] [DecidableEq C]
        {p : A → ℝ} {q : B → ℝ} (hp : p ∈ probabilitySimplex A) (hq : q ∈ probabilitySimplex B)
        (f : A → C) (g : B → C) (hcompat : ∀ c, fiberMass p f c = fiberMass q g c) :
        (fun z : {z : A × B // f z.1=g z.2} => jointLaw p q f g z.val) ∈
          probabilitySimplex {z : A × B // f z.1=g z.2} := by
    …

    Mentions: OAI.MatchingEntropy.probabilitySimplex, OAI.MatchingEntropy.fiberMass, OAI.MatchingEntropy.jointLaw

11. theorem OAI.MatchingEntropy.fiberMass_sum line 117
12. theorem OAI.MatchingEntropy.fiberMass_expect line 123
13. theorem OAI.MatchingEntropy.fiberMass_mem_simplex line 134
14. theorem OAI.MatchingEntropy.jointLaw_expect_first line 139
15. theorem OAI.MatchingEntropy.jointLaw_expect_second line 146
16. theorem OAI.MatchingEntropy.compatible_jointLaw_expect_first line 153
17. theorem OAI.MatchingEntropy.compatible_jointLaw_expect_second line 163