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 of edges of a relation between two finsets of vertices.
Instances For
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.
Instances For
theorem
Rel.mk_mem_interedges_iff
{α : Type u_4}
{β : Type u_5}
{r : α → β → Prop}
[(a : α) → DecidablePred (r a)]
{s : Finset α}
{t : Finset β}
{a : α}
{b : β}
:
@[simp]
theorem
Rel.interedges_empty_left
{α : Type u_4}
{β : Type u_5}
{r : α → β → Prop}
[(a : α) → DecidablePred (r a)]
(t : Finset β)
:
Rel.interedges r ∅ t = ∅
theorem
Rel.interedges_mono
{α : Type u_4}
{β : Type u_5}
{r : α → β → Prop}
[(a : α) → DecidablePred (r a)]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset β}
{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 : α) → DecidablePred (r a)]
(s : Finset α)
(t : Finset β)
:
Finset.card (Rel.interedges r s t) + Finset.card (Rel.interedges (fun x y => ¬r x y) s t) = Finset.card s * Finset.card t
theorem
Rel.interedges_disjoint_left
{α : Type u_4}
{β : Type u_5}
(r : α → β → Prop)
[(a : α) → DecidablePred (r a)]
{s : Finset α}
{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 : α) → DecidablePred (r a)]
(s : Finset α)
{t : Finset β}
{t' : Finset β}
(ht : Disjoint t t')
:
Disjoint (Rel.interedges r s t) (Rel.interedges r s t')
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 α)
:
Rel.interedges r (Finset.biUnion s f) 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)]
[DecidableEq α]
[DecidableEq β]
(s : Finset α)
(t : Finset ι)
(f : ι → Finset β)
:
Rel.interedges r s (Finset.biUnion t f) = 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)]
[DecidableEq α]
[DecidableEq β]
(s : Finset ι)
(t : Finset κ)
(f : ι → Finset α)
(g : κ → Finset β)
:
Rel.interedges r (Finset.biUnion s f) (Finset.biUnion t g) = Finset.biUnion (s ×ˢ t) fun ab => Rel.interedges r (f ab.fst) (g ab.snd)
theorem
Rel.card_interedges_le_mul
{α : Type u_4}
{β : Type u_5}
(r : α → β → Prop)
[(a : α) → DecidablePred (r a)]
(s : Finset α)
(t : Finset β)
:
Finset.card (Rel.interedges r s t) ≤ Finset.card s * Finset.card t
theorem
Rel.edgeDensity_nonneg
{α : Type u_4}
{β : Type u_5}
(r : α → β → Prop)
[(a : α) → DecidablePred (r a)]
(s : Finset α)
(t : Finset β)
:
0 ≤ Rel.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 β)
:
Rel.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 : Finset.Nonempty s)
(ht : Finset.Nonempty t)
:
Rel.edgeDensity r s t + 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 : Finset β)
:
Rel.edgeDensity r ∅ t = 0
@[simp]
theorem
Rel.edgeDensity_empty_right
{α : Type u_4}
{β : Type u_5}
(r : α → β → Prop)
[(a : α) → DecidablePred (r a)]
(s : Finset α)
:
Rel.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 β)
:
Finset.card (Rel.interedges r s t) = Finset.sum P.parts fun a => Finset.card (Rel.interedges r a t)
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)
:
Finset.card (Rel.interedges r s t) = Finset.sum P.parts fun b => Finset.card (Rel.interedges r s b)
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)
:
Finset.card (Rel.interedges r s t) = Finset.sum (P.parts ×ˢ Q.parts) fun ab => Finset.card (Rel.interedges r ab.fst ab.snd)
theorem
Rel.mul_edgeDensity_le_edgeDensity
{α : Type u_4}
{β : Type u_5}
(r : α → β → Prop)
[(a : α) → DecidablePred (r a)]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset β}
{t₂ : Finset β}
(hs : s₂ ⊆ s₁)
(ht : t₂ ⊆ t₁)
(hs₂ : Finset.Nonempty s₂)
(ht₂ : Finset.Nonempty t₂)
:
↑(Finset.card s₂) / ↑(Finset.card s₁) * (↑(Finset.card t₂) / ↑(Finset.card t₁)) * 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₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset β}
{t₂ : Finset β}
(hs : s₂ ⊆ s₁)
(ht : t₂ ⊆ t₁)
(hs₂ : Finset.Nonempty s₂)
(ht₂ : Finset.Nonempty t₂)
:
Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁ ≤ 1 - ↑(Finset.card s₂) / ↑(Finset.card s₁) * (↑(Finset.card t₂) / ↑(Finset.card t₁))
theorem
Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul
{α : Type u_4}
{β : Type u_5}
(r : α → β → Prop)
[(a : α) → DecidablePred (r a)]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset β}
{t₂ : Finset β}
(hs : s₂ ⊆ s₁)
(ht : t₂ ⊆ t₁)
(hs₂ : Finset.Nonempty s₂)
(ht₂ : Finset.Nonempty t₂)
:
|Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁| ≤ 1 - ↑(Finset.card s₂) / ↑(Finset.card s₁) * (↑(Finset.card t₂) / ↑(Finset.card t₁))
theorem
Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq
{𝕜 : Type u_1}
{α : Type u_4}
{β : Type u_5}
[LinearOrderedField 𝕜]
(r : α → β → Prop)
[(a : α) → DecidablePred (r a)]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset β}
{t₂ : Finset β}
{δ : 𝕜}
(hs : s₂ ⊆ s₁)
(ht : t₂ ⊆ t₁)
(hδ₀ : 0 ≤ δ)
(hδ₁ : δ < 1)
(hs₂ : (1 - δ) * ↑(Finset.card s₁) ≤ ↑(Finset.card s₂))
(ht₂ : (1 - δ) * ↑(Finset.card t₁) ≤ ↑(Finset.card t₂))
:
|↑(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}
[LinearOrderedField 𝕜]
(r : α → β → Prop)
[(a : α) → DecidablePred (r a)]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset β}
{t₂ : Finset β}
{δ : 𝕜}
(hs : s₂ ⊆ s₁)
(ht : t₂ ⊆ t₁)
(hδ : 0 ≤ δ)
(hscard : (1 - δ) * ↑(Finset.card s₁) ≤ ↑(Finset.card s₂))
(htcard : (1 - δ) * ↑(Finset.card t₁) ≤ ↑(Finset.card t₂))
:
|↑(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}
[DecidableRel r]
{s : Finset α}
{t : Finset α}
(hr : Symmetric r)
{x : α × α}
:
Prod.swap x ∈ Rel.interedges r s t ↔ x ∈ Rel.interedges r t s
theorem
Rel.mk_mem_interedges_comm
{α : Type u_4}
{r : α → α → Prop}
[DecidableRel r]
{s : Finset α}
{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}
[DecidableRel r]
(hr : Symmetric r)
(s : Finset α)
(t : Finset α)
:
Finset.card (Rel.interedges r s t) = Finset.card (Rel.interedges r t s)
theorem
Rel.edgeDensity_comm
{α : Type u_4}
{r : α → α → Prop}
[DecidableRel r]
(hr : Symmetric r)
(s : Finset α)
(t : Finset α)
:
Rel.edgeDensity r s t = Rel.edgeDensity r t s
Density of a graph #
def
SimpleGraph.interedges
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(s : Finset α)
(t : Finset α)
:
Finset of edges of a relation between two finsets of vertices.
Instances For
Density of edges of a graph between two finsets of vertices.
Instances For
theorem
SimpleGraph.interedges_def
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(s : Finset α)
(t : Finset α)
:
SimpleGraph.interedges G s t = Finset.filter (fun e => SimpleGraph.Adj G e.fst e.snd) (s ×ˢ t)
theorem
SimpleGraph.edgeDensity_def
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(s : Finset α)
(t : Finset α)
:
SimpleGraph.edgeDensity G s t = ↑(Finset.card (SimpleGraph.interedges G s t)) / (↑(Finset.card s) * ↑(Finset.card t))
@[simp]
theorem
SimpleGraph.card_interedges_div_card
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(s : Finset α)
(t : Finset α)
:
↑(Finset.card (SimpleGraph.interedges G s t)) / (↑(Finset.card s) * ↑(Finset.card t)) = SimpleGraph.edgeDensity G s t
theorem
SimpleGraph.mem_interedges_iff
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{s : Finset α}
{t : Finset α}
{x : α × α}
:
x ∈ SimpleGraph.interedges G s t ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ SimpleGraph.Adj G x.fst x.snd
theorem
SimpleGraph.mk_mem_interedges_iff
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{s : Finset α}
{t : Finset α}
{a : α}
{b : α}
:
(a, b) ∈ SimpleGraph.interedges G s t ↔ a ∈ s ∧ b ∈ t ∧ SimpleGraph.Adj G a b
@[simp]
theorem
SimpleGraph.interedges_empty_left
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(t : Finset α)
:
SimpleGraph.interedges G ∅ t = ∅
theorem
SimpleGraph.interedges_mono
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
s₂ ⊆ s₁ → t₂ ⊆ t₁ → SimpleGraph.interedges G s₂ t₂ ⊆ SimpleGraph.interedges G s₁ t₁
theorem
SimpleGraph.interedges_disjoint_left
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{s₁ : Finset α}
{s₂ : Finset α}
(hs : Disjoint s₁ s₂)
(t : Finset α)
:
Disjoint (SimpleGraph.interedges G s₁ t) (SimpleGraph.interedges G s₂ t)
theorem
SimpleGraph.interedges_disjoint_right
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{t₁ : Finset α}
{t₂ : Finset α}
(s : Finset α)
(ht : Disjoint t₁ t₂)
:
Disjoint (SimpleGraph.interedges G s t₁) (SimpleGraph.interedges G 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 α)
:
SimpleGraph.interedges G (Finset.biUnion s f) t = Finset.biUnion s fun a => SimpleGraph.interedges G (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 α)
:
SimpleGraph.interedges G s (Finset.biUnion 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 : SimpleGraph α)
[DecidableRel G.Adj]
[DecidableEq α]
(s : Finset ι)
(t : Finset κ)
(f : ι → Finset α)
(g : κ → Finset α)
:
SimpleGraph.interedges G (Finset.biUnion s f) (Finset.biUnion t g) = Finset.biUnion (s ×ˢ t) fun ab => SimpleGraph.interedges G (f ab.fst) (g ab.snd)
theorem
SimpleGraph.card_interedges_add_card_interedges_compl
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{s : Finset α}
{t : Finset α}
[DecidableEq α]
(h : Disjoint s t)
:
Finset.card (SimpleGraph.interedges G s t) + Finset.card (SimpleGraph.interedges Gᶜ s t) = Finset.card s * Finset.card t
theorem
SimpleGraph.edgeDensity_add_edgeDensity_compl
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{s : Finset α}
{t : Finset α}
[DecidableEq α]
(hs : Finset.Nonempty s)
(ht : Finset.Nonempty t)
(h : Disjoint s t)
:
SimpleGraph.edgeDensity G s t + SimpleGraph.edgeDensity Gᶜ s t = 1
theorem
SimpleGraph.card_interedges_le_mul
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(s : Finset α)
(t : Finset α)
:
Finset.card (SimpleGraph.interedges G s t) ≤ Finset.card s * Finset.card t
theorem
SimpleGraph.edgeDensity_nonneg
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(s : Finset α)
(t : Finset α)
:
0 ≤ SimpleGraph.edgeDensity G s t
theorem
SimpleGraph.edgeDensity_le_one
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(s : Finset α)
(t : Finset α)
:
SimpleGraph.edgeDensity G s t ≤ 1
@[simp]
theorem
SimpleGraph.edgeDensity_empty_left
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(t : Finset α)
:
SimpleGraph.edgeDensity G ∅ t = 0
@[simp]
theorem
SimpleGraph.edgeDensity_empty_right
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(s : Finset α)
:
SimpleGraph.edgeDensity G s ∅ = 0
@[simp]
theorem
SimpleGraph.swap_mem_interedges_iff
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{s : Finset α}
{t : Finset α}
{x : α × α}
:
Prod.swap x ∈ SimpleGraph.interedges G s t ↔ x ∈ SimpleGraph.interedges G t s
theorem
SimpleGraph.mk_mem_interedges_comm
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{s : Finset α}
{t : Finset α}
{a : α}
{b : α}
:
(a, b) ∈ SimpleGraph.interedges G s t ↔ (b, a) ∈ SimpleGraph.interedges G t s
theorem
SimpleGraph.edgeDensity_comm
{α : Type u_4}
(G : SimpleGraph α)
[DecidableRel G.Adj]
(s : Finset α)
(t : Finset α)
:
SimpleGraph.edgeDensity G s t = SimpleGraph.edgeDensity G t s