# Graph uniformity and uniform partitions #

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 #

• SimpleGraph.IsUniform: Graph uniformity of a pair of finsets of vertices.
• SimpleGraph.nonuniformWitness: G.nonuniformWitness ε s t and G.nonuniformWitness ε t s together witness the non-uniformity of s and t.
• Finpartition.nonUniforms: Non uniform pairs of parts of a partition.
• Finpartition.IsUniform: Uniformity of a partition.
• Finpartition.nonuniformWitnesses: 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 SimpleGraph.IsUniform {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] (ε : 𝕜) (s : ) (t : ) :

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
• G.IsUniform ε s t = ∀ ⦃s' : ⦄, s' s∀ ⦃t' : ⦄, t' ts.card * ε s'.cardt.card * ε t'.card|(G.edgeDensity s' t') - (G.edgeDensity s t)| < ε
Instances For
instance SimpleGraph.IsUniform.instDecidableRel {α : Type u_1} {𝕜 : Type u_2} {G : } [DecidableRel G.Adj] {ε : 𝕜} :
DecidableRel (G.IsUniform ε)
Equations
• SimpleGraph.IsUniform.instDecidableRel = id inferInstance
theorem SimpleGraph.IsUniform.mono {α : Type u_1} {𝕜 : Type u_2} {G : } [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } {ε' : 𝕜} (h : ε ε') (hε : G.IsUniform ε s t) :
G.IsUniform ε' s t
theorem SimpleGraph.IsUniform.symm {α : Type u_1} {𝕜 : Type u_2} {G : } [DecidableRel G.Adj] {ε : 𝕜} :
Symmetric (G.IsUniform ε)
theorem SimpleGraph.isUniform_comm {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } :
G.IsUniform ε s t G.IsUniform ε t s
theorem SimpleGraph.isUniform_one {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {s : } {t : } :
G.IsUniform 1 s t
theorem SimpleGraph.IsUniform.pos {α : Type u_1} {𝕜 : Type u_2} {G : } [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (hG : G.IsUniform ε s t) :
0 < ε
@[simp]
theorem SimpleGraph.isUniform_singleton {α : Type u_1} {𝕜 : Type u_2} {G : } [DecidableRel G.Adj] {ε : 𝕜} {a : α} {b : α} :
G.IsUniform ε {a} {b} 0 < ε
theorem SimpleGraph.not_isUniform_zero {α : Type u_1} {𝕜 : Type u_2} {G : } [DecidableRel G.Adj] {s : } {t : } :
¬G.IsUniform 0 s t
theorem SimpleGraph.not_isUniform_iff {α : Type u_1} {𝕜 : Type u_2} {G : } [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } :
¬G.IsUniform ε s t s's, t't, s.card * ε s'.card t.card * ε t'.card ε |G.edgeDensity s' t' - G.edgeDensity s t|
noncomputable def SimpleGraph.nonuniformWitnesses {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] (ε : 𝕜) (s : ) (t : ) :
×

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 SimpleGraph.nonuniformWitness.

Equations
• G.nonuniformWitnesses ε s t = if h : ¬G.IsUniform ε s t then (.choose, .choose) else (s, t)
Instances For
theorem SimpleGraph.left_nonuniformWitnesses_subset {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (h : ¬G.IsUniform ε s t) :
(G.nonuniformWitnesses ε s t).1 s
theorem SimpleGraph.left_nonuniformWitnesses_card {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (h : ¬G.IsUniform ε s t) :
s.card * ε (G.nonuniformWitnesses ε s t).1.card
theorem SimpleGraph.right_nonuniformWitnesses_subset {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (h : ¬G.IsUniform ε s t) :
(G.nonuniformWitnesses ε s t).2 t
theorem SimpleGraph.right_nonuniformWitnesses_card {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (h : ¬G.IsUniform ε s t) :
t.card * ε (G.nonuniformWitnesses ε s t).2.card
theorem SimpleGraph.nonuniformWitnesses_spec {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (h : ¬G.IsUniform ε s t) :
ε |G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|
noncomputable def SimpleGraph.nonuniformWitness {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] (ε : 𝕜) (s : ) (t : ) :

Arbitrary witness of non-uniformity. G.nonuniformWitness ε s t and G.nonuniformWitness ε t s form a pair of subsets witnessing the non-uniformity of (s, t). If (s, t) is uniform, returns s.

Equations
• G.nonuniformWitness ε s t = if then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2
Instances For
theorem SimpleGraph.nonuniformWitness_subset {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (h : ¬G.IsUniform ε s t) :
G.nonuniformWitness ε s t s
theorem SimpleGraph.le_card_nonuniformWitness {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (h : ¬G.IsUniform ε s t) :
s.card * ε (G.nonuniformWitness ε s t).card
theorem SimpleGraph.nonuniformWitness_spec {α : Type u_1} {𝕜 : Type u_2} (G : ) [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (h₁ : s t) (h₂ : ¬G.IsUniform ε s t) :
ε |G.edgeDensity (G.nonuniformWitness ε s t) (G.nonuniformWitness ε t s) - G.edgeDensity s t|

### Uniform partitions #

def Finpartition.sparsePairs {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] (ε : 𝕜) :

The pairs of parts of a partition P which are not ε-dense in a graph G. Note that we dismiss the diagonal. We do not care whether s is ε-dense with itself.

Equations
• P.sparsePairs G ε = Finset.filter (fun (x : × ) => match x with | (u, v) => (G.edgeDensity u v) < ε) P.parts.offDiag
Instances For
@[simp]
theorem Finpartition.mk_mem_sparsePairs {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] (u : ) (v : ) (ε : 𝕜) :
(u, v) P.sparsePairs G ε u P.parts v P.parts u v (G.edgeDensity u v) < ε
theorem Finpartition.sparsePairs_mono {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] {ε : 𝕜} {ε' : 𝕜} (h : ε ε') :
P.sparsePairs G ε P.sparsePairs G ε'
def Finpartition.nonUniforms {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel 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.nonUniforms G ε = Finset.filter (fun (x : × ) => match x with | (u, v) => ¬G.IsUniform ε u v) P.parts.offDiag
Instances For
@[simp]
theorem Finpartition.mk_mem_nonUniforms {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] {ε : 𝕜} {u : } {v : } :
(u, v) P.nonUniforms G ε u P.parts v P.parts u v ¬G.IsUniform ε u v
theorem Finpartition.nonUniforms_mono {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] {ε : 𝕜} {ε' : 𝕜} (h : ε ε') :
P.nonUniforms G ε' P.nonUniforms G ε
theorem Finpartition.nonUniforms_bot {α : Type u_1} {𝕜 : Type u_2} [] {A : } (G : ) [DecidableRel G.Adj] {ε : 𝕜} (hε : 0 < ε) :
.nonUniforms G ε =
def Finpartition.IsUniform {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] (ε : 𝕜) :

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
• P.IsUniform G ε = ((P.nonUniforms G ε).card (P.parts.card * (P.parts.card - 1)) * ε)
Instances For
theorem Finpartition.bot_isUniform {α : Type u_1} {𝕜 : Type u_2} [] {A : } (G : ) [DecidableRel G.Adj] {ε : 𝕜} (hε : 0 < ε) :
.IsUniform G ε
theorem Finpartition.isUniform_one {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] :
P.IsUniform G 1
theorem Finpartition.IsUniform.mono {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} {ε' : 𝕜} (hP : P.IsUniform G ε) (h : ε ε') :
P.IsUniform G ε'
theorem Finpartition.isUniformOfEmpty {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} (hP : P.parts = ) :
P.IsUniform G ε
theorem Finpartition.nonempty_of_not_uniform {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} (h : ¬P.IsUniform G ε) :
P.parts.Nonempty
noncomputable def Finpartition.nonuniformWitnesses {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] (ε : 𝕜) (s : ) :

A choice of witnesses of non-uniformity among the parts of a finpartition.

Equations
Instances For
theorem Finpartition.nonuniformWitness_mem_nonuniformWitnesses {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} {s : } {t : } (h : ¬G.IsUniform ε s t) (ht : t P.parts) (hst : s t) :
G.nonuniformWitness ε s t P.nonuniformWitnesses G ε s

### Equipartitions #

theorem Finpartition.IsEquipartition.card_interedges_sparsePairs_le' {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} (hP : P.IsEquipartition) (hε : 0 ε) :
((P.sparsePairs G ε).biUnion fun (x : × ) => match x with | (U, V) => G.interedges U V).card ε * (A.card + P.parts.card) ^ 2
theorem Finpartition.IsEquipartition.card_interedges_sparsePairs_le {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} (hP : P.IsEquipartition) (hε : 0 ε) :
((P.sparsePairs G ε).biUnion fun (x : × ) => match x with | (U, V) => G.interedges U V).card 4 * ε * A.card ^ 2
theorem Finpartition.IsEquipartition.card_biUnion_offDiag_le' {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } (hP : P.IsEquipartition) :
(P.parts.biUnion Finset.offDiag).card A.card * (A.card + P.parts.card) / P.parts.card
theorem Finpartition.IsEquipartition.card_biUnion_offDiag_le {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {ε : 𝕜} (hε : 0 < ε) (hP : P.IsEquipartition) (hP' : 4 / ε P.parts.card) :
(P.parts.biUnion Finset.offDiag).card ε / 2 * A.card ^ 2
theorem Finpartition.IsEquipartition.sum_nonUniforms_lt' {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} (hA : A.Nonempty) (hε : 0 < ε) (hP : P.IsEquipartition) (hG : P.IsUniform G ε) :
iP.nonUniforms G ε, i.1.card * i.2.card < ε * (A.card + P.parts.card) ^ 2
theorem Finpartition.IsEquipartition.sum_nonUniforms_lt {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} (hA : A.Nonempty) (hε : 0 < ε) (hP : P.IsEquipartition) (hG : P.IsUniform G ε) :
((P.nonUniforms G ε).biUnion fun (x : × ) => match x with | (U, V) => U ×ˢ V).card < 4 * ε * A.card ^ 2

### Reduced graph #

@[simp]
theorem SimpleGraph.regularityReduced_adj {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] (ε : 𝕜) (δ : 𝕜) (a : α) (b : α) :
.Adj a b = (G.Adj a b UP.parts, VP.parts, a U b V U V G.IsUniform ε U V δ (G.edgeDensity U V))
def SimpleGraph.regularityReduced {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] (ε : 𝕜) (δ : 𝕜) :

The reduction of the graph G along partition P has edges between ε-uniform pairs of parts that have edge density at least δ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance SimpleGraph.regularityReduced.instDecidableRel_adj {α : Type u_1} {𝕜 : Type u_2} [] {A : } (P : ) (G : ) [DecidableRel G.Adj] {ε : 𝕜} {δ : 𝕜} :
Equations
• = id inferInstance
theorem SimpleGraph.regularityReduced_le {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} {δ : 𝕜} :
G
theorem SimpleGraph.regularityReduced_mono {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {δ : 𝕜} {ε₁ : 𝕜} {ε₂ : 𝕜} (hε : ε₁ ε₂) :
theorem SimpleGraph.regularityReduced_anti {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} {δ₁ : 𝕜} {δ₂ : 𝕜} (hδ : δ₁ δ₂) :
theorem SimpleGraph.unreduced_edges_subset {α : Type u_1} {𝕜 : Type u_2} [] {A : } {P : } {G : } [DecidableRel G.Adj] {ε : 𝕜} :
Finset.filter (fun (x : α × α) => match x with | (x, y) => G.Adj x y ¬(SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).Adj x y) (A ×ˢ A) ((P.nonUniforms G (ε / 8)).biUnion fun (x : × ) => match x with | (U, V) => U ×ˢ V) P.parts.biUnion Finset.offDiag (P.sparsePairs G (ε / 4)).biUnion fun (x : × ) => match x with | (U, V) => G.interedges U V