# mathlib3documentation

combinatorics.simple_graph.density

# Edge density #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the number and density of edges of a relation/graph.

## Main declarations #

Between two finsets of vertices,

• rel.interedges: Finset of edges of a relation.
• rel.edge_density: Edge density of a relation.
• simple_graph.interedges: Finset of edges of a graph.
• simple_graph.edge_density: Edge density of a graph.

### Density of a relation #

def rel.interedges {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] (s : finset α) (t : finset β) :
finset × β)

Finset of edges of a relation between two finsets of vertices.

Equations
def rel.edge_density {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] (s : finset α) (t : finset β) :

Edge density of a relation between two finsets of vertices.

Equations
theorem rel.mem_interedges_iff {α : Type u_4} {β : Type u_5} {r : α β Prop} [Π (a : α), decidable_pred (r a)] {s : finset α} {t : finset β} {x : α × β} :
x t x.fst s x.snd t r x.fst x.snd
theorem rel.mk_mem_interedges_iff {α : Type u_4} {β : Type u_5} {r : α β Prop} [Π (a : α), decidable_pred (r a)] {s : finset α} {t : finset β} {a : α} {b : β} :
(a, b) t a s b t r a b
@[simp]
theorem rel.interedges_empty_left {α : Type u_4} {β : Type u_5} {r : α β Prop} [Π (a : α), decidable_pred (r a)] (t : finset β) :
t =
theorem rel.interedges_mono {α : Type u_4} {β : Type u_5} {r : α β Prop} [Π (a : α), decidable_pred (r a)] {s₁ s₂ : finset α} {t₁ t₂ : finset β} (hs : s₂ s₁) (ht : t₂ t₁) :
s₂ t₂ s₁ t₁
theorem rel.card_interedges_add_card_interedges_compl {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] (s : finset α) (t : finset β) :
s t).card + (rel.interedges (λ (x : α) (y : β), ¬r x y) s t).card = s.card * t.card
theorem rel.interedges_disjoint_left {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {s s' : finset α} (hs : s') (t : finset β) :
disjoint s t) s' t)
theorem rel.interedges_disjoint_right {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] (s : finset α) {t t' : finset β} (ht : t') :
disjoint s t) s t')
theorem rel.interedges_bUnion_left {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] [decidable_eq α] [decidable_eq β] (s : finset ι) (t : finset β) (f : ι ) :
(s.bUnion f) t = s.bUnion (λ (a : ι), (f a) t)
theorem rel.interedges_bUnion_right {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset ι) (f : ι ) :
(t.bUnion f) = t.bUnion (λ (b : ι), (f b))
theorem rel.interedges_bUnion {ι : Type u_2} {κ : Type u_3} {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] [decidable_eq α] [decidable_eq β] (s : finset ι) (t : finset κ) (f : ι ) (g : κ ) :
(s.bUnion f) (t.bUnion g) = (s ×ˢ t).bUnion (λ (ab : ι × κ), (f ab.fst) (g ab.snd))
theorem rel.card_interedges_le_mul {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] (s : finset α) (t : finset β) :
s t).card s.card * t.card
theorem rel.edge_density_nonneg {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] (s : finset α) (t : finset β) :
0 t
theorem rel.edge_density_le_one {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] (s : finset α) (t : finset β) :
t 1
theorem rel.edge_density_add_edge_density_compl {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {s : finset α} {t : finset β} (hs : s.nonempty) (ht : t.nonempty) :
t + rel.edge_density (λ (x : α) (y : β), ¬r x y) s t = 1
@[simp]
theorem rel.edge_density_empty_left {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] (t : finset β) :
= 0
@[simp]
theorem rel.edge_density_empty_right {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] (s : finset α) :
= 0
theorem rel.card_interedges_finpartition_left {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {s : finset α} [decidable_eq α] (P : finpartition s) (t : finset β) :
s t).card = P.parts.sum (λ (a : finset α), a t).card)
theorem rel.card_interedges_finpartition_right {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {t : finset β} [decidable_eq β] (s : finset α) (P : finpartition t) :
s t).card = P.parts.sum (λ (b : finset β), s b).card)
theorem rel.card_interedges_finpartition {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {s : finset α} {t : finset β} [decidable_eq α] [decidable_eq β] (P : finpartition s) (Q : finpartition t) :
s t).card = (P.parts ×ˢ Q.parts).sum (λ (ab : × finset β), ab.fst ab.snd).card)
theorem rel.mul_edge_density_le_edge_density {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {s₁ s₂ : finset α} {t₁ t₂ : finset β} (hs : s₂ s₁) (ht : t₂ t₁) (hs₂ : s₂.nonempty) (ht₂ : t₂.nonempty) :
(s₂.card) / (s₁.card) * ((t₂.card) / (t₁.card)) * s₂ t₂ s₁ t₁
theorem rel.edge_density_sub_edge_density_le_one_sub_mul {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {s₁ s₂ : finset α} {t₁ t₂ : finset β} (hs : s₂ s₁) (ht : t₂ t₁) (hs₂ : s₂.nonempty) (ht₂ : t₂.nonempty) :
s₂ t₂ - s₁ t₁ 1 - (s₂.card) / (s₁.card) * ((t₂.card) / (t₁.card))
theorem rel.abs_edge_density_sub_edge_density_le_one_sub_mul {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {s₁ s₂ : finset α} {t₁ t₂ : finset β} (hs : s₂ s₁) (ht : t₂ t₁) (hs₂ : s₂.nonempty) (ht₂ : t₂.nonempty) :
| s₂ t₂ - s₁ t₁| 1 - (s₂.card) / (s₁.card) * ((t₂.card) / (t₁.card))
theorem rel.abs_edge_density_sub_edge_density_le_two_mul_sub_sq {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {s₁ s₂ : finset α} {t₁ t₂ : finset β} {δ : 𝕜} (hs : s₂ s₁) (ht : t₂ t₁) (hδ₀ : 0 δ) (hδ₁ : δ < 1) (hs₂ : (1 - δ) * (s₁.card) (s₂.card)) (ht₂ : (1 - δ) * (t₁.card) (t₂.card)) :
| s₂ t₂) - s₁ t₁)| 2 * δ - δ ^ 2
theorem rel.abs_edge_density_sub_edge_density_le_two_mul {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} (r : α β Prop) [Π (a : α), decidable_pred (r a)] {s₁ s₂ : finset α} {t₁ t₂ : finset β} {δ : 𝕜} (hs : s₂ s₁) (ht : t₂ t₁) (hδ : 0 δ) (hscard : (1 - δ) * (s₁.card) (s₂.card)) (htcard : (1 - δ) * (t₁.card) (t₂.card)) :
| s₂ t₂) - s₁ t₁)| 2 * δ

If s₂ ⊆ s₁, t₂ ⊆ t₁ and they take up all but a δ-proportion, then the difference in edge densities is at most 2 * δ.

@[simp]
theorem rel.swap_mem_interedges_iff {α : Type u_4} {r : α α Prop} {s t : finset α} (hr : symmetric r) {x : α × α} :
x.swap t x s
theorem rel.mk_mem_interedges_comm {α : Type u_4} {r : α α Prop} {s t : finset α} {a b : α} (hr : symmetric r) :
(a, b) t (b, a) s
theorem rel.card_interedges_comm {α : Type u_4} {r : α α Prop} (hr : symmetric r) (s t : finset α) :
s t).card = t s).card
theorem rel.edge_density_comm {α : Type u_4} {r : α α Prop} (hr : symmetric r) (s t : finset α) :
t = s

### Density of a graph #

def simple_graph.interedges {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (s t : finset α) :
finset × α)

Finset of edges of a relation between two finsets of vertices.

Equations

Density of edges of a graph between two finsets of vertices.

Equations
theorem simple_graph.interedges_def {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (s t : finset α) :
G.interedges s t = finset.filter (λ (e : α × α), G.adj e.fst e.snd) (s ×ˢ t)
theorem simple_graph.edge_density_def {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (s t : finset α) :
G.edge_density s t = ((G.interedges s t).card) / ((s.card) * (t.card))
@[simp]
theorem simple_graph.card_interedges_div_card {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (s t : finset α) :
((G.interedges s t).card) / ((s.card) * (t.card)) = G.edge_density s t
theorem simple_graph.mem_interedges_iff {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] {s t : finset α} {x : α × α} :
x G.interedges s t x.fst s x.snd t G.adj x.fst x.snd
theorem simple_graph.mk_mem_interedges_iff {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] {s t : finset α} {a b : α} :
(a, b) G.interedges s t a s b t G.adj a b
@[simp]
theorem simple_graph.interedges_empty_left {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (t : finset α) :
t =
theorem simple_graph.interedges_mono {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] {s₁ s₂ t₁ t₂ : finset α} :
s₂ s₁ t₂ t₁ G.interedges s₂ t₂ G.interedges s₁ t₁
theorem simple_graph.interedges_disjoint_left {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] {s₁ s₂ : finset α} (hs : disjoint s₁ s₂) (t : finset α) :
disjoint (G.interedges s₁ t) (G.interedges s₂ t)
theorem simple_graph.interedges_disjoint_right {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] {t₁ t₂ : finset α} (s : finset α) (ht : disjoint t₁ t₂) :
disjoint (G.interedges s t₁) (G.interedges s t₂)
theorem simple_graph.interedges_bUnion_left {ι : Type u_2} {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] [decidable_eq α] (s : finset ι) (t : finset α) (f : ι ) :
G.interedges (s.bUnion f) t = s.bUnion (λ (a : ι), G.interedges (f a) t)
theorem simple_graph.interedges_bUnion_right {ι : Type u_2} {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] [decidable_eq α] (s : finset α) (t : finset ι) (f : ι ) :
G.interedges s (t.bUnion f) = t.bUnion (λ (b : ι), G.interedges s (f b))
theorem simple_graph.interedges_bUnion {ι : Type u_2} {κ : Type u_3} {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] [decidable_eq α] (s : finset ι) (t : finset κ) (f : ι ) (g : κ ) :
G.interedges (s.bUnion f) (t.bUnion g) = (s ×ˢ t).bUnion (λ (ab : ι × κ), G.interedges (f ab.fst) (g ab.snd))
theorem simple_graph.edge_density_add_edge_density_compl {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] {s t : finset α} [decidable_eq α] (hs : s.nonempty) (ht : t.nonempty) (h : t) :
G.edge_density s t + t = 1
theorem simple_graph.card_interedges_le_mul {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (s t : finset α) :
theorem simple_graph.edge_density_nonneg {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (s t : finset α) :
theorem simple_graph.edge_density_le_one {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (s t : finset α) :
@[simp]
theorem simple_graph.edge_density_empty_left {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (t : finset α) :
t = 0
@[simp]
@[simp]
theorem simple_graph.swap_mem_interedges_iff {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] {s t : finset α} {x : α × α} :
theorem simple_graph.mk_mem_interedges_comm {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] {s t : finset α} {a b : α} :
(a, b) G.interedges s t (b, a) G.interedges t s
theorem simple_graph.edge_density_comm {α : Type u_4} (G : simple_graph α) [decidable_rel G.adj] (s t : finset α) :

Extension for the positivity tactic: rel.edge_density and simple_graph.edge_density are always nonnegative.