Related-pair counts between finsets

Facts about Mathlib's Rel.interedges and Rel.edgeDensity used when comparing edge densities across a refinement of finite partitions: the edge count between two finsets is their size product times their edge density (with no nonemptiness hypothesis, since both sides vanish on an empty finset), edge counts are additive over disjoint unions on either side, and the edge count between two finsets splits along the traces of the parts of finite partitions on them. The corresponding SimpleGraph results are specializations to the adjacency relation. Edge densities are invariant under relabelling the vertices along an equivalence (SimpleGraph.edgeDensity_comap_symm).

For graphs, SimpleGraph.patternDensity G e s t is the edge density of (s, t) if e holds and the nonedge density 1 - d(s, t) otherwise: the density factor of a pair in the predicted count of an induced pattern. It lies in [0, 1] and changes by exactly as much as the edge density.

theorem Rel.card_mul_card_mul_edgeDensity {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) : ↑s.card * ↑t.card * edgeDensity r s t = ↑(interedges r s t).card

The number of related pairs between two finsets is their size product times their density. This holds without nonemptiness hypotheses: if either finset is empty, both sides vanish.

theorem Rel.card_mul_card_mul_edgeDensity_real {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) : ↑s.card * ↑t.card * ↑(edgeDensity r s t) = ↑(interedges r s t).card

The real-valued form of Rel.card_mul_card_mul_edgeDensity.

theorem Rel.card_interedges_biUnion_left {α : Type u_1} {β : Type u_2} {ι : Type u_3} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] [DecidableEq α] (s : Finset ι) (t : Finset β) (f : ι → Finset α) (hf : (↑s).PairwiseDisjoint f) : (interedges r (s.biUnion f) t).card = ∑ i ∈ s, (interedges r (f i) t).card

Related-pair counts are additive over a pairwise disjoint union on the left.

theorem Rel.card_interedges_biUnion_right {α : Type u_1} {β : Type u_2} {ι : Type u_3} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] [DecidableEq β] (s : Finset α) (t : Finset ι) (f : ι → Finset β) (hf : (↑t).PairwiseDisjoint f) : (interedges r s (t.biUnion f)).card = ∑ i ∈ t, (interedges r s (f i)).card

Related-pair counts are additive over a pairwise disjoint union on the right.

theorem Rel.card_interedges_eq_sum_parts {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] [DecidableEq α] [DecidableEq β] {s A : Finset α} {t B : Finset β} (P : Finpartition s) (Q : Finpartition t) (hA : A ⊆ s) (hB : B ⊆ t) : (interedges r A B).card = ∑ C ∈ P.parts, ∑ D ∈ Q.parts, (interedges r (A ∩ C) (B ∩ D)).card

The number of related pairs between A ⊆ s and B ⊆ t splits along the traces on A and on B of the parts of finite partitions of s and of t.

theorem Rel.sum_sum_card_interedges_fiber {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] {P Q : Finpartition s} {P' Q' : Finpartition t} (h : Q ≤ P) (h' : Q' ≤ P') (A : ↥P.parts) (C : ↥P'.parts) : ∑ B : ↥Q.parts with Finpartition.refinementParent h B = A, ∑ D : ↥Q'.parts with Finpartition.refinementParent h' D = C, (interedges r ↑B ↑D).card = (interedges r ↑A ↑C).card

The related-pair count between two coarse parts is the sum of the counts between the fine parts with those coarse parents.

theorem Rel.sum_sum_card_interedges_fiber_real {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] {P Q : Finpartition s} {P' Q' : Finpartition t} (h : Q ≤ P) (h' : Q' ≤ P') (A : ↥P.parts) (C : ↥P'.parts) : ∑ B : ↥Q.parts with Finpartition.refinementParent h B = A, ∑ D : ↥Q'.parts with Finpartition.refinementParent h' D = C, ↑(interedges r ↑B ↑D).card = ↑(interedges r ↑A ↑C).card

The real-valued form of Rel.sum_sum_card_interedges_fiber.

theorem SimpleGraph.card_mul_card_mul_edgeDensity {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (s t : Finset V) : ↑s.card * ↑t.card * G.edgeDensity s t = ↑(G.interedges s t).card

The number of edges between two finsets is their size product times their edge density. This holds without nonemptiness hypotheses: if either finset is empty, both sides vanish.

theorem SimpleGraph.card_mul_card_mul_edgeDensity_real {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (s t : Finset V) : ↑s.card * ↑t.card * ↑(G.edgeDensity s t) = ↑(G.interedges s t).card

The real-valued form of SimpleGraph.card_mul_card_mul_edgeDensity.

@[simp]

theorem SimpleGraph.edgeDensity_comap_symm {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] {W : Type u_3} (e : V ≃ W) (s t : Finset V) : (SimpleGraph.comap (⇑e.symm) G).edgeDensity (Finset.map e.toEmbedding s) (Finset.map e.toEmbedding t) = G.edgeDensity s t

Edge densities are invariant under relabelling. Relabelling the vertices along e, the graph as G.comap e.symm and both finsets by mapping along e, leaves the edge density unchanged.

noncomputable def SimpleGraph.patternDensity {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] {𝕜 : Type u_3} [DivisionRing 𝕜] (e : Prop) [Decidable e] (s t : Finset V) : 𝕜

The edge density of (s, t) if e holds, and its nonedge density 1 - d(s, t) otherwise. This is the density factor of a pair in the predicted count of an induced pattern, where e records whether the pattern has an edge there.

theorem SimpleGraph.patternDensity_def {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] {𝕜 : Type u_3} [DivisionRing 𝕜] (e : Prop) [Decidable e] (s t : Finset V) : G.patternDensity e s t = if e then ↑(G.edgeDensity s t) else 1 - ↑(G.edgeDensity s t)

@[simp]

theorem SimpleGraph.patternDensity_of_pos {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] {𝕜 : Type u_3} [DivisionRing 𝕜] {e : Prop} [Decidable e] (he : e) (s t : Finset V) : G.patternDensity e s t = ↑(G.edgeDensity s t)

Where the pattern has an edge, its density factor is the edge density.

@[simp]

theorem SimpleGraph.patternDensity_of_neg {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] {𝕜 : Type u_3} [DivisionRing 𝕜] {e : Prop} [Decidable e] (he : ¬e) (s t : Finset V) : G.patternDensity e s t = 1 - ↑(G.edgeDensity s t)

Where the pattern has no edge, its density factor is the nonedge density.

theorem SimpleGraph.patternDensity_nonneg {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] {𝕜 : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (e : Prop) [Decidable e] (s t : Finset V) : 0 ≤ G.patternDensity e s t

An edge or nonedge density is nonnegative.

theorem SimpleGraph.patternDensity_le_one {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] {𝕜 : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (e : Prop) [Decidable e] (s t : Finset V) : G.patternDensity e s t ≤ 1

An edge or nonedge density is at most one.

theorem SimpleGraph.abs_patternDensity_sub {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] {𝕜 : Type u_3} [Field 𝕜] [LinearOrder 𝕜] (e : Prop) [Decidable e] (s t s' t' : Finset V) : |G.patternDensity e s t - G.patternDensity e s' t'| = |↑(G.edgeDensity s t) - ↑(G.edgeDensity s' t')|

An edge or nonedge density changes by exactly as much as the edge density.

theorem SimpleGraph.card_interedges_biUnion_left {V : Type u_1} {ι : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (s : Finset ι) (t : Finset V) (f : ι → Finset V) (hf : (↑s).PairwiseDisjoint f) : (G.interedges (s.biUnion f) t).card = ∑ i ∈ s, (G.interedges (f i) t).card

Edge counts are additive over a pairwise disjoint union on the left.

theorem SimpleGraph.card_interedges_biUnion_right {V : Type u_1} {ι : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (s : Finset V) (t : Finset ι) (f : ι → Finset V) (hf : (↑t).PairwiseDisjoint f) : (G.interedges s (t.biUnion f)).card = ∑ i ∈ t, (G.interedges s (f i)).card

Edge counts are additive over a pairwise disjoint union on the right.

theorem SimpleGraph.card_interedges_eq_sum_parts {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] {s t A B : Finset V} (P : Finpartition s) (Q : Finpartition t) (hA : A ⊆ s) (hB : B ⊆ t) : (G.interedges A B).card = ∑ C ∈ P.parts, ∑ D ∈ Q.parts, (G.interedges (A ∩ C) (B ∩ D)).card

The number of edges between A ⊆ s and B ⊆ t splits along the traces on A and on B of the parts of finite partitions of s and of t.

theorem SimpleGraph.sum_sum_card_interedges_fiber {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] {s : Finset V} {P Q : Finpartition s} (h : Q ≤ P) (A C : ↥P.parts) : ∑ B : ↥Q.parts with Finpartition.refinementParent h B = A, ∑ D : ↥Q.parts with Finpartition.refinementParent h D = C, (G.interedges ↑B ↑D).card = (G.interedges ↑A ↑C).card

The edge count between two coarse parts is the sum of the edge counts between the fine parts with those coarse parents.

theorem SimpleGraph.sum_sum_card_interedges_fiber_real {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] {s : Finset V} {P Q : Finpartition s} (h : Q ≤ P) (A C : ↥P.parts) : ∑ B : ↥Q.parts with Finpartition.refinementParent h B = A, ∑ D : ↥Q.parts with Finpartition.refinementParent h D = C, ↑(G.interedges ↑B ↑D).card = ↑(G.interedges ↑A ↑C).card

The real-valued form of SimpleGraph.sum_sum_card_interedges_fiber.