# Edge density #

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.edgeDensity: Edge density of a relation.
• SimpleGraph.interedges: Finset of edges of a graph.
• SimpleGraph.edgeDensity: Edge density of a graph.

### Density of a relation #

def Rel.interedges {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : ) (t : ) :
Finset (α × β)

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

Equations
Instances For
def Rel.edgeDensity {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : ) (t : ) :

Edge density of a relation between two finsets of vertices.

Equations
• = ().card / (s.card * t.card)
Instances For
theorem Rel.mem_interedges_iff {α : Type u_4} {β : Type u_5} {r : αβProp} [(a : α) → DecidablePred (r a)] {s : } {t : } {x : α × β} :
x x.1 s x.2 t r x.1 x.2
theorem Rel.mk_mem_interedges_iff {α : Type u_4} {β : Type u_5} {r : αβProp} [(a : α) → DecidablePred (r a)] {s : } {t : } {a : α} {b : β} :
(a, b) a s b t r a b
@[simp]
theorem Rel.interedges_empty_left {α : Type u_4} {β : Type u_5} {r : αβProp} [(a : α) → DecidablePred (r a)] (t : ) :
theorem Rel.interedges_mono {α : Type u_4} {β : Type u_5} {r : αβProp} [(a : α) → DecidablePred (r a)] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (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 : α) → DecidablePred (r a)] (s : ) (t : ) :
().card + (Rel.interedges (fun (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 : α) → DecidablePred (r a)] {s : } {s' : } (hs : Disjoint s s') (t : ) :
theorem Rel.interedges_disjoint_right {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : ) {t : } {t' : } (ht : Disjoint t t') :
theorem Rel.interedges_biUnion_left {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] [] [] (s : ) (t : ) (f : ι) :
Rel.interedges r () t = Finset.biUnion s fun (a : ι) => Rel.interedges r (f a) t
theorem Rel.interedges_biUnion_right {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] [] [] (s : ) (t : ) (f : ι) :
Rel.interedges r s () = Finset.biUnion t fun (b : ι) => Rel.interedges r s (f b)
theorem Rel.interedges_biUnion {ι : Type u_2} {κ : Type u_3} {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] [] [] (s : ) (t : ) (f : ι) (g : κ) :
Rel.interedges r () () = Finset.biUnion (s ×ˢ t) fun (ab : ι × κ) => Rel.interedges r (f ab.1) (g ab.2)
theorem Rel.card_interedges_le_mul {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : ) (t : ) :
().card s.card * t.card
theorem Rel.edgeDensity_nonneg {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : ) (t : ) :
0
theorem Rel.edgeDensity_le_one {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : ) (t : ) :
1
theorem Rel.edgeDensity_add_edgeDensity_compl {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) :
+ Rel.edgeDensity (fun (x : α) (y : β) => ¬r x y) s t = 1
@[simp]
theorem Rel.edgeDensity_empty_left {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (t : ) :
= 0
@[simp]
theorem Rel.edgeDensity_empty_right {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : ) :
= 0
theorem Rel.card_interedges_finpartition_left {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s : } [] (P : ) (t : ) :
().card = Finset.sum P.parts fun (a : ) => ().card
theorem Rel.card_interedges_finpartition_right {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {t : } [] (s : ) (P : ) :
().card = Finset.sum P.parts fun (b : ) => ().card
theorem Rel.card_interedges_finpartition {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s : } {t : } [] [] (P : ) (Q : ) :
().card = Finset.sum (P.parts ×ˢ Q.parts) fun (ab : × ) => (Rel.interedges r ab.1 ab.2).card
theorem Rel.mul_edgeDensity_le_edgeDensity {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₂ s₁) (ht : t₂ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) :
s₂.card / s₁.card * (t₂.card / t₁.card) * Rel.edgeDensity r s₂ t₂ Rel.edgeDensity r s₁ t₁
theorem Rel.edgeDensity_sub_edgeDensity_le_one_sub_mul {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₂ s₁) (ht : t₂ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) :
Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁ 1 - s₂.card / s₁.card * (t₂.card / t₁.card)
theorem Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₂ s₁) (ht : t₂ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) :
|Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁| 1 - s₂.card / s₁.card * (t₂.card / t₁.card)
theorem Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : } {s₂ : } {t₁ : } {t₂ : } {δ : 𝕜} (hs : s₂ s₁) (ht : t₂ t₁) (hδ₀ : 0 δ) (hδ₁ : δ < 1) (hs₂ : (1 - δ) * s₁.card s₂.card) (ht₂ : (1 - δ) * t₁.card t₂.card) :
|(Rel.edgeDensity r s₂ t₂) - (Rel.edgeDensity r s₁ t₁)| 2 * δ - δ ^ 2
theorem Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : } {s₂ : } {t₁ : } {t₂ : } {δ : 𝕜} (hs : s₂ s₁) (ht : t₂ t₁) (hδ : 0 δ) (hscard : (1 - δ) * s₁.card s₂.card) (htcard : (1 - δ) * t₁.card t₂.card) :
|(Rel.edgeDensity r s₂ t₂) - (Rel.edgeDensity 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} [] {s : } {t : } (hr : ) {x : α × α} :
x
theorem Rel.mk_mem_interedges_comm {α : Type u_4} {r : ααProp} [] {s : } {t : } {a : α} {b : α} (hr : ) :
(a, b) (b, a)
theorem Rel.card_interedges_comm {α : Type u_4} {r : ααProp} [] (hr : ) (s : ) (t : ) :
().card = ().card
theorem Rel.edgeDensity_comm {α : Type u_4} {r : ααProp} [] (hr : ) (s : ) (t : ) :
=

### Density of a graph #

def SimpleGraph.interedges {α : Type u_4} (G : ) [DecidableRel G.Adj] (s : ) (t : ) :
Finset (α × α)

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

Equations
Instances For
def SimpleGraph.edgeDensity {α : Type u_4} (G : ) [DecidableRel G.Adj] :

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

Equations
Instances For
theorem SimpleGraph.interedges_def {α : Type u_4} (G : ) [DecidableRel G.Adj] (s : ) (t : ) :
= Finset.filter (fun (e : α × α) => G.Adj e.1 e.2) (s ×ˢ t)
theorem SimpleGraph.edgeDensity_def {α : Type u_4} (G : ) [DecidableRel G.Adj] (s : ) (t : ) :
= ().card / (s.card * t.card)
@[simp]
theorem SimpleGraph.card_interedges_div_card {α : Type u_4} (G : ) [DecidableRel G.Adj] (s : ) (t : ) :
().card / (s.card * t.card) =
theorem SimpleGraph.mem_interedges_iff {α : Type u_4} (G : ) [DecidableRel G.Adj] {s : } {t : } {x : α × α} :
x x.1 s x.2 t G.Adj x.1 x.2
theorem SimpleGraph.mk_mem_interedges_iff {α : Type u_4} (G : ) [DecidableRel G.Adj] {s : } {t : } {a : α} {b : α} :
(a, b) a s b t G.Adj a b
@[simp]
theorem SimpleGraph.interedges_empty_left {α : Type u_4} (G : ) [DecidableRel G.Adj] (t : ) :
theorem SimpleGraph.interedges_mono {α : Type u_4} (G : ) [DecidableRel G.Adj] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₂ s₁t₂ t₁
theorem SimpleGraph.interedges_disjoint_left {α : Type u_4} (G : ) [DecidableRel G.Adj] {s₁ : } {s₂ : } (hs : Disjoint s₁ s₂) (t : ) :
Disjoint () ()
theorem SimpleGraph.interedges_disjoint_right {α : Type u_4} (G : ) [DecidableRel G.Adj] {t₁ : } {t₂ : } (s : ) (ht : Disjoint t₁ t₂) :
Disjoint () ()
theorem SimpleGraph.interedges_biUnion_left {ι : Type u_2} {α : Type u_4} (G : ) [DecidableRel G.Adj] [] (s : ) (t : ) (f : ι) :
= Finset.biUnion s fun (a : ι) => SimpleGraph.interedges G (f a) t
theorem SimpleGraph.interedges_biUnion_right {ι : Type u_2} {α : Type u_4} (G : ) [DecidableRel G.Adj] [] (s : ) (t : ) (f : ι) :
= Finset.biUnion t fun (b : ι) => SimpleGraph.interedges G s (f b)
theorem SimpleGraph.interedges_biUnion {ι : Type u_2} {κ : Type u_3} {α : Type u_4} (G : ) [DecidableRel G.Adj] [] (s : ) (t : ) (f : ι) (g : κ) :
SimpleGraph.interedges G () () = Finset.biUnion (s ×ˢ t) fun (ab : ι × κ) => SimpleGraph.interedges G (f ab.1) (g ab.2)
theorem SimpleGraph.card_interedges_add_card_interedges_compl {α : Type u_4} (G : ) [DecidableRel G.Adj] {s : } {t : } [] (h : Disjoint s t) :
().card + ().card = s.card * t.card
theorem SimpleGraph.edgeDensity_add_edgeDensity_compl {α : Type u_4} (G : ) [DecidableRel G.Adj] {s : } {t : } [] (hs : s.Nonempty) (ht : t.Nonempty) (h : Disjoint s t) :
+ = 1
theorem SimpleGraph.card_interedges_le_mul {α : Type u_4} (G : ) [DecidableRel G.Adj] (s : ) (t : ) :
().card s.card * t.card
theorem SimpleGraph.edgeDensity_nonneg {α : Type u_4} (G : ) [DecidableRel G.Adj] (s : ) (t : ) :
0
theorem SimpleGraph.edgeDensity_le_one {α : Type u_4} (G : ) [DecidableRel G.Adj] (s : ) (t : ) :
1
@[simp]
theorem SimpleGraph.edgeDensity_empty_left {α : Type u_4} (G : ) [DecidableRel G.Adj] (t : ) :
@[simp]
theorem SimpleGraph.edgeDensity_empty_right {α : Type u_4} (G : ) [DecidableRel G.Adj] (s : ) :
@[simp]
theorem SimpleGraph.swap_mem_interedges_iff {α : Type u_4} (G : ) [DecidableRel G.Adj] {s : } {t : } {x : α × α} :
x
theorem SimpleGraph.mk_mem_interedges_comm {α : Type u_4} (G : ) [DecidableRel G.Adj] {s : } {t : } {a : α} {b : α} :
(a, b) (b, a)
theorem SimpleGraph.edgeDensity_comm {α : Type u_4} (G : ) [DecidableRel G.Adj] (s : ) (t : ) :
=