structure NonnegDependence.Matching (X : Type u_3) (Y : Type u_4) [DecidableEq X] [DecidableEq Y] : Type (max u_3 u_4)

A bipartite matching between $X$ and $Y$: a finite set of edges $(x, y)$ such that no two edges share a left endpoint or a right endpoint.

• edges : Finset (X × Y)
• left_inj ⦃e₁ e₂ : X × Y⦄ : e₁ ∈ self.edges → e₂ ∈ self.edges → e₁.1 = e₂.1 → e₁ = e₂
• right_inj ⦃e₁ e₂ : X × Y⦄ : e₁ ∈ self.edges → e₂ ∈ self.edges → e₁.2 = e₂.2 → e₁ = e₂

@[implicit_reducible]

instance NonnegDependence.instDecidableEqMatching {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] : DecidableEq (Matching X Y)

Decidable equality on matchings reduces to decidable equality on their underlying edge sets.

def NonnegDependence.Matching.leftVerts {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] (F : Matching X Y) : Finset X

The set of left endpoints covered by the matching $F$.

def NonnegDependence.Matching.rightVerts {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] (F : Matching X Y) : Finset Y

The set of right endpoints covered by the matching $F$.

def NonnegDependence.extendsMatching {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] (f : X ↪ Y) (F : Matching X Y) : Prop

The injection $f : X \hookrightarrow Y$ extends the matching $F$ if $f(x) = y$ for every edge $(x, y) \in F$.

@[implicit_reducible]

instance NonnegDependence.decidableExtendsMatching {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] [Fintype X] [Fintype Y] (f : X ↪ Y) (F : Matching X Y) : Decidable (extendsMatching f F)

Decidability of extendsMatching, by reducing to a finite conjunction over the edges of F.

noncomputable def NonnegDependence.matchingsAvoiding {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] [Fintype X] [Fintype Y] (T : Matching X Y) (Fs : List (Matching X Y)) : Finset (X ↪ Y)

Injections $f : X \hookrightarrow Y$ that extend $T$ and avoid every matching in Fs.

noncomputable def NonnegDependence.avoidsAllSet {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] [Fintype X] [Fintype Y] (Fs : List (Matching X Y)) : Finset (X ↪ Y)

Injections $f : X \hookrightarrow Y$ that avoid every matching in Fs, with no further extension constraint.

def NonnegDependence.compPerm {X : Type u_1} {Y : Type u_2} (σ : Equiv.Perm Y) (f : X ↪ Y) : X ↪ Y

Postcomposition of an injection $f : X \hookrightarrow Y$ with a permutation $\sigma$ of $Y$, yielding the injection $x \mapsto \sigma(f(x))$.

theorem NonnegDependence.image_not_in_rightVerts {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] (f : X ↪ Y) (F : Matching X Y) (hext : extendsMatching f F) (x : X) (hx : x ∉ F.leftVerts) : f x ∉ F.rightVerts

If $f$ extends $F$ and $x \notin \text{leftVerts}(F)$, then $f(x) \notin \text{rightVerts}(F)$ (else injectivity of $f$ would force $x$ into $\text{leftVerts}(F)$).

theorem NonnegDependence.edges_eq_of_extends {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] {T₁ T₂ : Matching X Y} {f : X ↪ Y} (h1 : T₁.leftVerts = T₂.leftVerts) (hext1 : extendsMatching f T₁) (hext2 : extendsMatching f T₂) : T₁.edges = T₂.edges

Two matchings with the same left vertex set that are both extended by the same injection $f$ must have identical edge sets.

theorem NonnegDependence.exists_permutation_between_matchings {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] [Fintype Y] (F₀ T : Matching X Y) (hleft : T.leftVerts = F₀.leftVerts) : ∃ (σ : Equiv.Perm Y), (∀ e ∈ T.edges, ∃ e₀ ∈ F₀.edges, e₀.1 = e.1 ∧ σ e₀.2 = e.2) ∧ ∀ y ∉ F₀.rightVerts, σ y ∉ F₀.rightVerts → σ y = y

Given two matchings $F_0, T$ with the same left vertex set, there exists a permutation $\sigma$ of $Y$ that maps right endpoints of $F_0$ to the corresponding right endpoints of $T$ (per shared left vertex) and fixes every $y$ outside $\text{rightVerts}(F_0)$ whose image is also outside $\text{rightVerts}(F_0)$.

theorem NonnegDependence.nonneg_dependence_card_ineq {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] [Fintype X] [Fintype Y] (F₀ T : Matching X Y) (Fs : List (Matching X Y)) (σ : Equiv.Perm Y) (hσ_sends : ∀ e ∈ T.edges, ∃ e₀ ∈ F₀.edges, e₀.1 = e.1 ∧ σ e₀.2 = e.2) (hσ_fix : ∀ y ∉ F₀.rightVerts, σ y ∉ F₀.rightVerts → σ y = y) (hdisjL : ∀ G ∈ Fs, Disjoint F₀.leftVerts G.leftVerts) (hdisjR : ∀ G ∈ Fs, Disjoint F₀.rightVerts G.rightVerts) : (matchingsAvoiding F₀ Fs).card ≤ (matchingsAvoiding T Fs).card

Counting step toward nonnegative correlation: postcomposition with the permutation $\sigma$ provided by exists_permutation_between_matchings gives an injection from matchingsAvoiding F₀ Fs into matchingsAvoiding T Fs, hence $|\text{matchingsAvoiding}(F_0, Fs)| \le |\text{matchingsAvoiding}(T, Fs)|$.

theorem NonnegDependence.nonneg_dependence_prob_ineq {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] [Fintype X] [Fintype Y] (F₀ : Matching X Y) (Fs : List (Matching X Y)) (hdisjL : ∀ G ∈ Fs, Disjoint F₀.leftVerts G.leftVerts) (hdisjR : ∀ G ∈ Fs, Disjoint F₀.rightVerts G.rightVerts) (Ts : Finset (Matching X Y)) (hTs_left : ∀ T ∈ Ts, T.leftVerts = F₀.leftVerts) : (matchingsAvoiding F₀ Fs).card * Ts.card ≤ (avoidsAllSet Fs).card

Nonnegative-dependence inequality (Theorem 6.5.5, counting form): summing the previous inequality over a family Ts of matchings sharing the same left vertex set as $F_0$ and pairwise disjoint from the matchings in Fs yields $|\text{matchingsAvoiding}(F_0, Fs)| \cdot |Ts| \le |\text{avoidsAllSet}(Fs)|$. This is the combinatorial content of nonnegative correlation for random injections.