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} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) (s : Finset α) (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

• G.IsUniform ε s t = ∀ ⦃s' : Finset α⦄, s' ⊆ s → ∀ ⦃t' : Finset α⦄, t' ⊆ t → ↑s.card * ε ≤ ↑s'.card → ↑t.card * ε ≤ ↑t'.card → |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε

instance SimpleGraph.IsUniform.instDecidableRel {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} : DecidableRel (G.IsUniform ε)

Equations

• SimpleGraph.IsUniform.instDecidableRel = id inferInstance

theorem SimpleGraph.IsUniform.mono {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} {ε' : 𝕜} (h : ε ≤ ε') (hε : G.IsUniform ε s t) : G.IsUniform ε' s t

theorem SimpleGraph.IsUniform.symm {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} : Symmetric (G.IsUniform ε)

theorem SimpleGraph.isUniform_comm {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} : G.IsUniform ε s t ↔ G.IsUniform ε t s

theorem SimpleGraph.isUniform_one {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} : G.IsUniform 1 s t

theorem SimpleGraph.IsUniform.pos {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (hG : G.IsUniform ε s t) : 0 < ε

@[simp]

theorem SimpleGraph.isUniform_singleton {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {a : α} {b : α} : G.IsUniform ε {a} {b} ↔ 0 < ε

theorem SimpleGraph.not_isUniform_zero {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {s : Finset α} {t : Finset α} : ¬G.IsUniform 0 s t

theorem SimpleGraph.not_isUniform_iff {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} : ¬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} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) (s : Finset α) (t : Finset α) : Finset α × 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 SimpleGraph.nonuniformWitness.

Equations

• G.nonuniformWitnesses ε s t = if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)

theorem SimpleGraph.left_nonuniformWitnesses_subset {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (h : ¬G.IsUniform ε s t) : (G.nonuniformWitnesses ε s t).1 ⊆ s

theorem SimpleGraph.left_nonuniformWitnesses_card {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (h : ¬G.IsUniform ε s t) : ↑s.card * ε ≤ ↑(G.nonuniformWitnesses ε s t).1.card

theorem SimpleGraph.right_nonuniformWitnesses_subset {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (h : ¬G.IsUniform ε s t) : (G.nonuniformWitnesses ε s t).2 ⊆ t

theorem SimpleGraph.right_nonuniformWitnesses_card {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (h : ¬G.IsUniform ε s t) : ↑t.card * ε ≤ ↑(G.nonuniformWitnesses ε s t).2.card

theorem SimpleGraph.nonuniformWitnesses_spec {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (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} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) (s : Finset α) (t : Finset α) : Finset α

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 WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2

theorem SimpleGraph.nonuniformWitness_subset {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (h : ¬G.IsUniform ε s t) : G.nonuniformWitness ε s t ⊆ s

theorem SimpleGraph.le_card_nonuniformWitness {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (h : ¬G.IsUniform ε s t) : ↑s.card * ε ≤ ↑(G.nonuniformWitness ε s t).card

theorem SimpleGraph.nonuniformWitness_spec {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (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} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) : Finset (Finset α × Finset α)

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 : Finset α × Finset α) => match x with | (u, v) => ↑(G.edgeDensity u v) < ε) P.parts.offDiag

@[simp]

theorem Finpartition.mk_mem_sparsePairs {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (u : Finset α) (v : Finset α) (ε : 𝕜) : (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} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {ε' : 𝕜} (h : ε ≤ ε') : P.sparsePairs G ε ⊆ P.sparsePairs G ε'

def Finpartition.nonUniforms {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) : Finset (Finset α × Finset α)

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 : Finset α × Finset α) => match x with | (u, v) => ¬G.IsUniform ε u v) P.parts.offDiag

@[simp]

theorem Finpartition.mk_mem_nonUniforms {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {u : Finset α} {v : Finset α} : (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} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {ε' : 𝕜} (h : ε ≤ ε') : P.nonUniforms G ε' ⊆ P.nonUniforms G ε

theorem Finpartition.nonUniforms_bot {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} (hε : 0 < ε) : ⊥.nonUniforms G ε = ∅

def Finpartition.IsUniform {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel 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

• P.IsUniform G ε = (↑(P.nonUniforms G ε).card ≤ ↑(P.parts.card * (P.parts.card - 1)) * ε)

theorem Finpartition.bot_isUniform {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} (hε : 0 < ε) : ⊥.IsUniform G ε

theorem Finpartition.isUniform_one {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] : P.IsUniform G 1

theorem Finpartition.IsUniform.mono {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {ε' : 𝕜} (hP : P.IsUniform G ε) (h : ε ≤ ε') : P.IsUniform G ε'

theorem Finpartition.isUniformOfEmpty {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} (hP : P.parts = ∅) : P.IsUniform G ε

theorem Finpartition.nonempty_of_not_uniform {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} (h : ¬P.IsUniform G ε) : P.parts.Nonempty

noncomputable def Finpartition.nonuniformWitnesses {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) (s : Finset α) : Finset (Finset α)

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

Equations

• P.nonuniformWitnesses G ε s = Finset.image (G.nonuniformWitness ε s) (Finset.filter (fun (t : Finset α) => s ≠ t ∧ ¬G.IsUniform ε s t) P.parts)

theorem Finpartition.nonuniformWitness_mem_nonuniformWitnesses {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (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} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} (hP : P.IsEquipartition) (hε : 0 ≤ ε) : ↑((P.sparsePairs G ε).biUnion fun (x : Finset α × Finset α) => 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} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} (hP : P.IsEquipartition) (hε : 0 ≤ ε) : ↑((P.sparsePairs G ε).biUnion fun (x : Finset α × Finset α) => 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} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} (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} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {ε : 𝕜} (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} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} (hA : A.Nonempty) (hε : 0 < ε) (hP : P.IsEquipartition) (hG : P.IsUniform G ε) : ∑ i ∈ P.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} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} (hA : A.Nonempty) (hε : 0 < ε) (hP : P.IsEquipartition) (hG : P.IsUniform G ε) : ↑((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) => match x with | (U, V) => U ×ˢ V).card < 4 * ε * ↑A.card ^ 2

Reduced graph

def SimpleGraph.regularityReduced {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) (δ : 𝕜) : SimpleGraph α

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.

@[simp]

theorem SimpleGraph.regularityReduced_adj {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) (δ : 𝕜) (a : α) (b : α) : (SimpleGraph.regularityReduced P G ε δ).Adj a b = (G.Adj a b ∧ ∃ U ∈ P.parts, ∃ V ∈ P.parts, a ∈ U ∧ b ∈ V ∧ U ≠ V ∧ G.IsUniform ε U V ∧ δ ≤ ↑(G.edgeDensity U V))

instance SimpleGraph.regularityReduced.instDecidableRel_adj {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {δ : 𝕜} : DecidableRel (SimpleGraph.regularityReduced P G ε δ).Adj

Equations

• SimpleGraph.regularityReduced.instDecidableRel_adj P G = id inferInstance

theorem SimpleGraph.regularityReduced_le {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {δ : 𝕜} : SimpleGraph.regularityReduced P G ε δ ≤ G

theorem SimpleGraph.regularityReduced_mono {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {δ : 𝕜} {ε₁ : 𝕜} {ε₂ : 𝕜} (hε : ε₁ ≤ ε₂) : SimpleGraph.regularityReduced P G ε₁ δ ≤ SimpleGraph.regularityReduced P G ε₂ δ

theorem SimpleGraph.regularityReduced_anti {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {δ₁ : 𝕜} {δ₂ : 𝕜} (hδ : δ₁ ≤ δ₂) : SimpleGraph.regularityReduced P G ε δ₂ ≤ SimpleGraph.regularityReduced P G ε δ₁

theorem SimpleGraph.unreduced_edges_subset {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [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 : Finset α × Finset α) => match x with | (U, V) => U ×ˢ V) ∪ P.parts.biUnion Finset.offDiag ∪ (P.sparsePairs G (ε / 4)).biUnion fun (x : Finset α × Finset α) => match x with | (U, V) => G.interedges U V