Densities of coherent pair colors

pairColorDensity S c s t is the proportion of ordered distinct pairs in s ×ˢ t with color c. The denominator excludes the diagonal even when the cells overlap. An empty support has density zero; consequently the palette densities sum to one only when there is at least one distinct pair. Reversing the cells reverses the palette color.

These densities supply the pair factors in predictions for colored hypergraph counts.

noncomputable def TauCeti.pairColorDensity {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (c : κ) (s t : Finset V) : ℚ

The density of a color among the ordered distinct pairs in two finite vertex sets. It is zero when no distinct pair exists.

theorem TauCeti.pairColorDensity_def {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [DecidableEq V] (S : PairColorSystem κ V) (c : κ) (s t : Finset V) : pairColorDensity S c s t = ↑{p ∈ s ×ˢ t | S.colorOfPair p.1 p.2 = some c}.card / ↑{p ∈ s ×ˢ t | p.1 ≠ p.2}.card

Pair-color density is the color count divided by the distinct-pair count.

theorem TauCeti.pairColorDensity_mul_card_support {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [DecidableEq V] (S : PairColorSystem κ V) (c : κ) (s t : Finset V) : pairColorDensity S c s t * ↑{p ∈ s ×ˢ t | p.1 ≠ p.2}.card = ↑{p ∈ s ×ˢ t | S.colorOfPair p.1 p.2 = some c}.card

Multiplying density by the size of its distinct-pair support recovers the color count. This also holds for empty support, when both sides vanish.

theorem TauCeti.pairColorDensity_mul_card_of_disjoint {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (S : PairColorSystem κ V) (c : κ) {s t : Finset V} (hst : Disjoint s t) : pairColorDensity S c s t * (↑s.card * ↑t.card) = ↑{p ∈ s ×ˢ t | S.colorOfPair p.1 p.2 = some c}.card

For disjoint sets, every pair in s ×ˢ t is a distinct pair, so the density times #s * #t is the color count.

theorem TauCeti.pairColorDensity_eq_edgeDensity_of_disjoint {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (S : PairColorSystem κ V) (c : κ) {s t : Finset V} (hst : Disjoint s t) : pairColorDensity S c s t = Rel.edgeDensity (fun (x y : V) => S.colorOfPair x y = some c) s t

On disjoint sets, pair-color density agrees with the density of the relation selecting that color. This identifies the distinct-pair and Cartesian-product normalizations.

theorem TauCeti.pairColorDensity_nonneg {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (c : κ) (s t : Finset V) : 0 ≤ pairColorDensity S c s t

Pair-color densities are nonnegative.

theorem TauCeti.pairColorDensity_le_one {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (c : κ) (s t : Finset V) : pairColorDensity S c s t ≤ 1

A color occupies at most the whole distinct-pair support.

theorem TauCeti.pairColorDensity_eq_zero_of_support_eq_empty {κ : Type u_1} {V : Type u_2} [DecidableEq V] (S : PairColorSystem κ V) (c : κ) (s t : Finset V) (h : {p ∈ s ×ˢ t | p.1 ≠ p.2} = ∅) : pairColorDensity S c s t = 0

With no distinct pairs, every color has density zero.

@[simp]

theorem TauCeti.pairColorDensity_empty_left {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (c : κ) (t : Finset V) : pairColorDensity S c ∅ t = 0

@[simp]

theorem TauCeti.pairColorDensity_empty_right {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (c : κ) (s : Finset V) : pairColorDensity S c s ∅ = 0

@[simp]

theorem TauCeti.pairColorDensity_singleton_self {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (c : κ) (v : V) : pairColorDensity S c {v} {v} = 0

theorem TauCeti.sum_pairColorDensity {κ : Type u_1} {V : Type u_2} [Fintype κ] [DecidableEq V] (S : PairColorSystem κ V) (s t : Finset V) (h : {p ∈ s ×ˢ t | p.1 ≠ p.2}.Nonempty) : ∑ c : κ, pairColorDensity S c s t = 1

Palette densities sum to one on nonempty distinct-pair support. Nonempty cells alone do not suffice, as the coincident-singleton case shows.

theorem TauCeti.sum_pairColorDensity_le_one {κ : Type u_1} {V : Type u_2} [Fintype κ] (S : PairColorSystem κ V) (s t : Finset V) : ∑ c : κ, pairColorDensity S c s t ≤ 1

Palette densities sum to at most one: to one on nonempty distinct-pair support, and to zero otherwise.

theorem TauCeti.pairColorDensity_swap {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (c : κ) (s t : Finset V) : pairColorDensity S (S.rev c) t s = pairColorDensity S c s t

Reversing both the ordered cells and the palette color preserves density.

theorem TauCeti.pairColorDensity_congr {κ : Type u_3} {V : Type u_4} {S T : PairColorSystem κ V} {s t : Finset V} (h : ∀ x ∈ s, ∀ y ∈ t, S.colorOfPair x y = T.colorOfPair x y) (c : κ) : pairColorDensity S c s t = pairColorDensity T c s t

Pair-color density depends only on the colors on the tested rectangle.

@[simp]

theorem TauCeti.pairColorDensity_comap {κ : Type u_1} {V : Type u_2} {W : Type u_3} (S : PairColorSystem κ W) (f : V ↪ W) (c : κ) (s t : Finset V) : pairColorDensity (S.comap f) c s t = pairColorDensity S c (Finset.map f s) (Finset.map f t)

Restriction along an embedding preserves every pair-color density on the image sets, including overlapping sets and empty distinct-pair supports.