Graph uniformity and uniform partitions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define uniformity of a pair of vertices in a graph and uniformity of a partition of vertices of a graph. Both are also known as ε-regularity.
Finsets of vertices s and t are ε-uniform in a graph G if their edge density is at most
ε-far from the density of any big enough s' and t' where s' ⊆ s, t' ⊆ t.
The definition is pretty technical, but it amounts to the edges between s and t being "random"
The literature contains several definitions which are equivalent up to scaling ε by some constant
when the partition is equitable.
A partition P of the vertices is ε-uniform if the proportion of non ε-uniform pairs of parts
is less than ε.
Main declarations #
simple_graph.is_uniform: Graph uniformity of a pair of finsets of vertices.simple_graph.nonuniform_witness:G.nonuniform_witness ε s tandG.nonuniform_witness ε t stogether witness the non-uniformity ofsandt.finpartition.non_uniforms: Non uniform pairs of parts of a partition.finpartition.is_uniform: Uniformity of a partition.finpartition.nonuniform_witnesses: For each non-uniform pair of parts of a partition, pick witnesses of non-uniformity and dump them all together.
References #
Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean
Graph uniformity #
def
simple_graph.is_uniform
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
(ε : 𝕜)
(s t : finset α) :
Prop
A pair of finsets of vertices is ε-uniform (aka ε-regular) iff their edge density is close
to the density of any big enough pair of subsets. Intuitively, the edges between them are
random-like.
theorem
simple_graph.is_uniform.mono
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
{G : simple_graph α}
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
{ε' : 𝕜}
(h : ε ≤ ε')
(hε : G.is_uniform ε s t) :
G.is_uniform ε' s t
theorem
simple_graph.is_uniform.symm
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
{G : simple_graph α}
[decidable_rel G.adj]
{ε : 𝕜} :
symmetric (G.is_uniform ε)
theorem
simple_graph.is_uniform_comm
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α} :
G.is_uniform ε s t ↔ G.is_uniform ε t s
theorem
simple_graph.is_uniform_singleton
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{a b : α}
(hε : 0 < ε) :
G.is_uniform ε {a} {b}
theorem
simple_graph.not_is_uniform_zero
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{s t : finset α} :
¬G.is_uniform 0 s t
theorem
simple_graph.is_uniform_one
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{s t : finset α} :
G.is_uniform 1 s t
theorem
simple_graph.not_is_uniform_iff
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
{G : simple_graph α}
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α} :
noncomputable
def
simple_graph.nonuniform_witnesses
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
(ε : 𝕜)
(s t : finset α) :
An arbitrary pair of subsets witnessing the non-uniformity of (s, t). If (s, t) is uniform,
returns (s, t). Witnesses for (s, t) and (t, s) don't necessarily match. See
simple_graph.nonuniform_witness.
Equations
- G.nonuniform_witnesses ε s t = dite (¬G.is_uniform ε s t) (λ (h : ¬G.is_uniform ε s t), (_.some, _.some)) (λ (h : ¬¬G.is_uniform ε s t), (s, t))
theorem
simple_graph.left_nonuniform_witnesses_subset
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
(h : ¬G.is_uniform ε s t) :
(G.nonuniform_witnesses ε s t).fst ⊆ s
theorem
simple_graph.left_nonuniform_witnesses_card
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
(h : ¬G.is_uniform ε s t) :
theorem
simple_graph.right_nonuniform_witnesses_subset
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
(h : ¬G.is_uniform ε s t) :
(G.nonuniform_witnesses ε s t).snd ⊆ t
theorem
simple_graph.right_nonuniform_witnesses_card
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
(h : ¬G.is_uniform ε s t) :
theorem
simple_graph.nonuniform_witnesses_spec
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
(h : ¬G.is_uniform ε s t) :
ε ≤ |↑(G.edge_density (G.nonuniform_witnesses ε s t).fst (G.nonuniform_witnesses ε s t).snd) - ↑(G.edge_density s t)|
noncomputable
def
simple_graph.nonuniform_witness
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
(ε : 𝕜)
(s t : finset α) :
finset α
Arbitrary witness of non-uniformity. G.nonuniform_witness ε s t and
G.nonuniform_witness ε t s form a pair of subsets witnessing the non-uniformity of (s, t). If
(s, t) is uniform, returns s.
Equations
- G.nonuniform_witness ε s t = ite (well_ordering_rel s t) (G.nonuniform_witnesses ε s t).fst (G.nonuniform_witnesses ε t s).snd
theorem
simple_graph.nonuniform_witness_subset
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
(h : ¬G.is_uniform ε s t) :
G.nonuniform_witness ε s t ⊆ s
theorem
simple_graph.le_card_nonuniform_witness
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
(h : ¬G.is_uniform ε s t) :
theorem
simple_graph.nonuniform_witness_spec
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
(h₁ : s ≠ t)
(h₂ : ¬G.is_uniform ε s t) :
ε ≤ |↑(G.edge_density (G.nonuniform_witness ε s t) (G.nonuniform_witness ε t s)) - ↑(G.edge_density s t)|
Uniform partitions #
noncomputable
def
finpartition.non_uniforms
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
(P : finpartition A)
(G : simple_graph α)
[decidable_rel G.adj]
(ε : 𝕜) :
The pairs of parts of a partition P which are not ε-uniform in a graph G. Note that we
dismiss the diagonal. We do not care whether s is ε-uniform with itself.
Equations
- P.non_uniforms G ε = finset.filter (λ (uv : finset α × finset α), ¬G.is_uniform ε uv.fst uv.snd) P.parts.off_diag
theorem
finpartition.mk_mem_non_uniforms_iff
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
(P : finpartition A)
(G : simple_graph α)
[decidable_rel G.adj]
(u v : finset α)
(ε : 𝕜) :
theorem
finpartition.non_uniforms_mono
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
(P : finpartition A)
(G : simple_graph α)
[decidable_rel G.adj]
{ε ε' : 𝕜}
(h : ε ≤ ε') :
P.non_uniforms G ε' ⊆ P.non_uniforms G ε
theorem
finpartition.non_uniforms_bot
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
(hε : 0 < ε) :
⊥.non_uniforms G ε = ∅
def
finpartition.is_uniform
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
(P : finpartition A)
(G : simple_graph α)
[decidable_rel G.adj]
(ε : 𝕜) :
Prop
A finpartition of a graph's vertex set is ε-uniform (aka ε-regular) iff the proportion of
its pairs of parts that are not ε-uniform is at most ε.
theorem
finpartition.bot_is_uniform
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
(G : simple_graph α)
[decidable_rel G.adj]
{ε : 𝕜}
(hε : 0 < ε) :
⊥.is_uniform G ε
theorem
finpartition.is_uniform_one
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
(P : finpartition A)
(G : simple_graph α)
[decidable_rel G.adj] :
P.is_uniform G 1
theorem
finpartition.is_uniform.mono
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
{P : finpartition A}
{G : simple_graph α}
[decidable_rel G.adj]
{ε ε' : 𝕜}
(hP : P.is_uniform G ε)
(h : ε ≤ ε') :
P.is_uniform G ε'
theorem
finpartition.is_uniform_of_empty
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
{P : finpartition A}
{G : simple_graph α}
[decidable_rel G.adj]
{ε : 𝕜}
(hP : P.parts = ∅) :
P.is_uniform G ε
theorem
finpartition.nonempty_of_not_uniform
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
{P : finpartition A}
{G : simple_graph α}
[decidable_rel G.adj]
{ε : 𝕜}
(h : ¬P.is_uniform G ε) :
noncomputable
def
finpartition.nonuniform_witnesses
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
(P : finpartition A)
(G : simple_graph α)
[decidable_rel G.adj]
(ε : 𝕜)
(s : finset α) :
A choice of witnesses of non-uniformity among the parts of a finpartition.
Equations
- P.nonuniform_witnesses G ε s = finset.image (G.nonuniform_witness ε s) (finset.filter (λ (t : finset α), s ≠ t ∧ ¬G.is_uniform ε s t) P.parts)
theorem
finpartition.nonuniform_witness_mem_nonuniform_witnesses
{α : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_field 𝕜]
[decidable_eq α]
{A : finset α}
{P : finpartition A}
{G : simple_graph α}
[decidable_rel G.adj]
{ε : 𝕜}
{s t : finset α}
(h : ¬G.is_uniform ε s t)
(ht : t ∈ P.parts)
(hst : s ≠ t) :
G.nonuniform_witness ε s t ∈ P.nonuniform_witnesses G ε s