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 : Finset α) (t : Finset β) : Finset (α × β)

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

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

Edge density of a relation between two finsets of vertices.

theorem Rel.mem_interedges_iff {α : Type u_4} {β : Type u_5} {r : α → β → Prop} [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} {x : α × β} : x ∈ interedges r s t ↔ 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 : Finset α} {t : Finset β} {a : α} {b : β} : (a, b) ∈ interedges r s t ↔ 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 : Finset β) : interedges r ∅ t = ∅

theorem Rel.interedges_mono {α : Type u_4} {β : Type u_5} {r : α → β → Prop} [(a : α) → DecidablePred (r a)] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) : interedges r s₂ t₂ ⊆ 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 : Finset α) (t : Finset β) : (interedges r s t).card + (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' : Finset α} (hs : Disjoint s s') (t : Finset β) : Disjoint (interedges r s t) (interedges r s' t)

theorem Rel.interedges_disjoint_right {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] (s : Finset α) {t t' : Finset β} (ht : Disjoint t t') : Disjoint (interedges r s t) (interedges r s t')

theorem Rel.interedges_eq_biUnion {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] : interedges r s t = s.biUnion fun (x : α) => Finset.map { toFun := fun (x_1 : β) => (x, x_1), inj' := ⋯ } ({y ∈ t | r x y})

theorem Rel.interedges_biUnion_left {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] [DecidableEq α] [DecidableEq β] (s : Finset ι) (t : Finset β) (f : ι → Finset α) : interedges r (s.biUnion f) t = s.biUnion fun (a : ι) => 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)] [DecidableEq α] [DecidableEq β] (s : Finset α) (t : Finset ι) (f : ι → Finset β) : interedges r s (t.biUnion f) = t.biUnion fun (b : ι) => 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)] [DecidableEq α] [DecidableEq β] (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset β) : interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun (ab : ι × κ) => 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 : Finset α) (t : Finset β) : (interedges r s t).card ≤ s.card * t.card

theorem Rel.edgeDensity_nonneg {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) : 0 ≤ edgeDensity r s t

theorem Rel.edgeDensity_le_one {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) : edgeDensity r s t ≤ 1

theorem Rel.edgeDensity_add_edgeDensity_compl {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} (hs : s.Nonempty) (ht : t.Nonempty) : edgeDensity r s t + 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 : Finset β) : edgeDensity r ∅ t = 0

@[simp]

theorem Rel.edgeDensity_empty_right {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] (s : Finset α) : edgeDensity r s ∅ = 0

theorem Rel.card_interedges_finpartition_left {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] {s : Finset α} [DecidableEq α] (P : Finpartition s) (t : Finset β) : (interedges r s t).card = ∑ a ∈ P.parts, (interedges r a t).card

theorem Rel.card_interedges_finpartition_right {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] {t : Finset β} [DecidableEq β] (s : Finset α) (P : Finpartition t) : (interedges r s t).card = ∑ b ∈ P.parts, (interedges r s b).card

theorem Rel.card_interedges_finpartition {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] (P : Finpartition s) (Q : Finpartition t) : (interedges r s t).card = ∑ ab ∈ P.parts ×ˢ Q.parts, (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₂ : Finset α} {t₁ t₂ : Finset β} (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) : ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) * edgeDensity r s₂ t₂ ≤ 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₂ : Finset α} {t₁ t₂ : Finset β} (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) : edgeDensity r s₂ t₂ - 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₂ : Finset α} {t₁ t₂ : Finset β} (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) : |edgeDensity r s₂ t₂ - 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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (r : α → β → Prop) [(a : α) → DecidablePred (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) : |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2

theorem Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (r : α → β → Prop) [(a : α) → DecidablePred (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) : |↑(edgeDensity r s₂ t₂) - ↑(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} [DecidableRel r] {s t : Finset α} (hr : Symmetric r) {x : α × α} : x.swap ∈ interedges r s t ↔ x ∈ interedges r t s

theorem Rel.mk_mem_interedges_comm {α : Type u_4} {r : α → α → Prop} [DecidableRel r] {s t : Finset α} {a b : α} (hr : Symmetric r) : (a, b) ∈ interedges r s t ↔ (b, a) ∈ interedges r t s

theorem Rel.card_interedges_comm {α : Type u_4} {r : α → α → Prop} [DecidableRel r] (hr : Symmetric r) (s t : Finset α) : (interedges r s t).card = (interedges r t s).card

theorem Rel.edgeDensity_comm {α : Type u_4} {r : α → α → Prop} [DecidableRel r] (hr : Symmetric r) (s t : Finset α) : edgeDensity r s t = edgeDensity r t s

Density of a graph

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

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

def SimpleGraph.edgeDensity {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] : Finset α → Finset α → ℚ

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

theorem SimpleGraph.interedges_def {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s t : Finset α) : G.interedges s t = {e ∈ s ×ˢ t | G.Adj e.1 e.2}

theorem SimpleGraph.edgeDensity_def {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s t : Finset α) : G.edgeDensity s t = ↑(G.interedges s t).card / (↑s.card * ↑t.card)

theorem SimpleGraph.card_interedges_div_card {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s t : Finset α) : ↑(G.interedges s t).card / (↑s.card * ↑t.card) = G.edgeDensity s t

theorem SimpleGraph.mem_interedges_iff {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s t : Finset α} {x : α × α} : x ∈ G.interedges s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ G.Adj x.1 x.2

theorem SimpleGraph.mk_mem_interedges_iff {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s t : Finset α} {a b : α} : (a, b) ∈ G.interedges s t ↔ a ∈ s ∧ b ∈ t ∧ G.Adj a b

@[simp]

theorem SimpleGraph.interedges_empty_left {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (t : Finset α) : G.interedges ∅ t = ∅

theorem SimpleGraph.interedges_mono {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s₁ s₂ t₁ t₂ : Finset α} : s₂ ⊆ s₁ → t₂ ⊆ t₁ → G.interedges s₂ t₂ ⊆ G.interedges s₁ t₁

theorem SimpleGraph.interedges_disjoint_left {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s₁ s₂ : Finset α} (hs : Disjoint s₁ s₂) (t : Finset α) : Disjoint (G.interedges s₁ t) (G.interedges s₂ t)

theorem SimpleGraph.interedges_disjoint_right {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {t₁ t₂ : Finset α} (s : Finset α) (ht : Disjoint t₁ t₂) : Disjoint (G.interedges s t₁) (G.interedges s t₂)

theorem SimpleGraph.interedges_biUnion_left {ι : Type u_2} {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] [DecidableEq α] (s : Finset ι) (t : Finset α) (f : ι → Finset α) : G.interedges (s.biUnion f) t = s.biUnion fun (a : ι) => G.interedges (f a) t

theorem SimpleGraph.interedges_biUnion_right {ι : Type u_2} {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] [DecidableEq α] (s : Finset α) (t : Finset ι) (f : ι → Finset α) : G.interedges s (t.biUnion f) = t.biUnion fun (b : ι) => G.interedges s (f b)

theorem SimpleGraph.interedges_biUnion {ι : Type u_2} {κ : Type u_3} {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] [DecidableEq α] (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset α) : G.interedges (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun (ab : ι × κ) => G.interedges (f ab.1) (g ab.2)

theorem SimpleGraph.card_interedges_add_card_interedges_compl {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s t : Finset α} [DecidableEq α] (h : Disjoint s t) : (G.interedges s t).card + (Gᶜ.interedges s t).card = s.card * t.card

theorem SimpleGraph.edgeDensity_add_edgeDensity_compl {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s t : Finset α} [DecidableEq α] (hs : s.Nonempty) (ht : t.Nonempty) (h : Disjoint s t) : G.edgeDensity s t + Gᶜ.edgeDensity s t = 1

theorem SimpleGraph.card_interedges_le_mul {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s t : Finset α) : (G.interedges s t).card ≤ s.card * t.card

theorem SimpleGraph.edgeDensity_nonneg {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s t : Finset α) : 0 ≤ G.edgeDensity s t

theorem SimpleGraph.edgeDensity_le_one {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s t : Finset α) : G.edgeDensity s t ≤ 1

@[simp]

theorem SimpleGraph.edgeDensity_empty_left {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (t : Finset α) : G.edgeDensity ∅ t = 0

@[simp]

theorem SimpleGraph.edgeDensity_empty_right {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) : G.edgeDensity s ∅ = 0

@[simp]

theorem SimpleGraph.swap_mem_interedges_iff {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s t : Finset α} {x : α × α} : x.swap ∈ G.interedges s t ↔ x ∈ G.interedges t s

theorem SimpleGraph.mk_mem_interedges_comm {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s t : Finset α} {a b : α} : (a, b) ∈ G.interedges s t ↔ (b, a) ∈ G.interedges t s

theorem SimpleGraph.edgeDensity_comm {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s t : Finset α) : G.edgeDensity s t = G.edgeDensity t s