mathlib3 documentation

combinatorics.simple_graph.regularity.uniform

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 #

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.

Equations
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] {ε : 𝕜} :
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 α} :
¬G.is_uniform ε s t (s' : finset α), s' s (t' : finset α), t' t (s.card) * ε (s'.card) (t.card) * ε (t'.card) ε |(G.edge_density s' t') - (G.edge_density s t)|
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
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) :
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) :
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) :
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 α) :

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
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) :
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) :
(s.card) * ε ((G.nonuniform_witness ε s t).card)
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) :

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
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 α) (ε : 𝕜) :
(u, v) P.non_uniforms G ε u P.parts v P.parts u v ¬G.is_uniform ε u v
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 : ε ε') :
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 < ε) :
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 ε.

Equations
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 < ε) :
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] :
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
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) :