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 of edges of a relation between two finsets of vertices.
Equations
- rel.interedges r s t = finset.filter (λ (e : α × β), r e.fst e.snd) (s ×ˢ t)
@[simp]
theorem
rel.interedges_empty_left
{α : Type u_4}
{β : Type u_5}
{r : α → β → Prop}
[Π (a : α), decidable_pred (r a)]
(t : finset β) :
rel.interedges r ∅ 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₁) :
rel.interedges r s₂ t₂ ⊆ rel.interedges r 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 β) :
(rel.interedges r 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 : disjoint s s')
(t : finset β) :
disjoint (rel.interedges r s t) (rel.interedges r 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 : disjoint t t') :
disjoint (rel.interedges r s t) (rel.interedges r 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 : ι → finset α) :
rel.interedges r (s.bUnion f) t = s.bUnion (λ (a : ι), rel.interedges r (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 : ι → finset β) :
rel.interedges r s (t.bUnion f) = t.bUnion (λ (b : ι), rel.interedges r s (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 : ι → finset α)
(g : κ → finset β) :
rel.interedges r (s.bUnion f) (t.bUnion g) = (s ×ˢ t).bUnion (λ (ab : ι × κ), rel.interedges r (f ab.fst) (g ab.snd))
theorem
rel.edge_density_nonneg
{α : Type u_4}
{β : Type u_5}
(r : α → β → Prop)
[Π (a : α), decidable_pred (r a)]
(s : finset α)
(t : finset β) :
0 ≤ rel.edge_density r s t
theorem
rel.edge_density_le_one
{α : Type u_4}
{β : Type u_5}
(r : α → β → Prop)
[Π (a : α), decidable_pred (r a)]
(s : finset α)
(t : finset β) :
rel.edge_density r s 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) :
rel.edge_density r s 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 β) :
rel.edge_density r ∅ t = 0
@[simp]
theorem
rel.edge_density_empty_right
{α : Type u_4}
{β : Type u_5}
(r : α → β → Prop)
[Π (a : α), decidable_pred (r a)]
(s : finset α) :
rel.edge_density r s ∅ = 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 β) :
(rel.interedges r s t).card = P.parts.sum (λ (a : finset α), (rel.interedges r 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) :
(rel.interedges r s t).card = P.parts.sum (λ (b : finset β), (rel.interedges r 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) :
theorem
rel.abs_edge_density_sub_edge_density_le_two_mul_sub_sq
{𝕜 : Type u_1}
{α : Type u_4}
{β : Type u_5}
[linear_ordered_field 𝕜]
(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)) :
theorem
rel.abs_edge_density_sub_edge_density_le_two_mul
{𝕜 : Type u_1}
{α : Type u_4}
{β : Type u_5}
[linear_ordered_field 𝕜]
(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)) :
|↑(rel.edge_density r s₂ t₂) - ↑(rel.edge_density r 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}
[decidable_rel r]
{s t : finset α}
(hr : symmetric r)
{x : α × α} :
x.swap ∈ rel.interedges r s t ↔ x ∈ rel.interedges r t s
theorem
rel.mk_mem_interedges_comm
{α : Type u_4}
{r : α → α → Prop}
[decidable_rel r]
{s t : finset α}
{a b : α}
(hr : symmetric r) :
(a, b) ∈ rel.interedges r s t ↔ (b, a) ∈ rel.interedges r t s
theorem
rel.card_interedges_comm
{α : Type u_4}
{r : α → α → Prop}
[decidable_rel r]
(hr : symmetric r)
(s t : finset α) :
(rel.interedges r s t).card = (rel.interedges r t s).card
theorem
rel.edge_density_comm
{α : Type u_4}
{r : α → α → Prop}
[decidable_rel r]
(hr : symmetric r)
(s t : finset α) :
rel.edge_density r s t = rel.edge_density r t s
Density of a graph #
def
simple_graph.interedges
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
(s t : finset α) :
Finset of edges of a relation between two finsets of vertices.
Equations
- G.interedges s t = rel.interedges G.adj s t
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 α) :
@[simp]
theorem
simple_graph.card_interedges_div_card
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
(s t : finset α) :
theorem
simple_graph.mem_interedges_iff
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
{s t : finset α}
{x : α × α} :
theorem
simple_graph.mk_mem_interedges_iff
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
{s t : finset α}
{a b : α} :
@[simp]
theorem
simple_graph.interedges_empty_left
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
(t : finset α) :
G.interedges ∅ 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 : ι → finset α) :
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 : ι → finset α) :
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 : ι → finset α)
(g : κ → finset α) :
G.interedges (s.bUnion f) (t.bUnion g) = (s ×ˢ t).bUnion (λ (ab : ι × κ), G.interedges (f ab.fst) (g ab.snd))
theorem
simple_graph.card_interedges_add_card_interedges_compl
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
{s t : finset α}
[decidable_eq α]
(h : disjoint s t) :
(G.interedges s t).card + (Gᶜ.interedges s t).card = s.card * t.card
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 : disjoint s t) :
G.edge_density s t + Gᶜ.edge_density s 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 α) :
0 ≤ G.edge_density s t
theorem
simple_graph.edge_density_le_one
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
(s t : finset α) :
G.edge_density s t ≤ 1
@[simp]
theorem
simple_graph.edge_density_empty_left
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
(t : finset α) :
G.edge_density ∅ t = 0
@[simp]
theorem
simple_graph.edge_density_empty_right
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
(s : finset α) :
G.edge_density s ∅ = 0
@[simp]
theorem
simple_graph.swap_mem_interedges_iff
{α : Type u_4}
(G : simple_graph α)
[decidable_rel G.adj]
{s t : finset α}
{x : α × α} :
x.swap ∈ G.interedges s t ↔ x ∈ G.interedges t s
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 α) :
G.edge_density s t = G.edge_density t s