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 ε-uniform pairs of parts is greater than (1 - ε).

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: Nonuniform 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][srl_itp]

Graph uniformity

def SimpleGraph.IsUniform {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] (G : SimpleGraph α) [DecidableRel 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.

@[implicit_reducible]

instance SimpleGraph.instDecidableIsUniform {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) (s t : Finset α) : Decidable (G.IsUniform ε s t)

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

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

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

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

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

@[simp]

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

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

theorem SimpleGraph.not_isUniform_iff {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s 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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) (s 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.

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

theorem SimpleGraph.left_nonuniformWitnesses_card {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s 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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α} (h : ¬G.IsUniform ε s t) : (G.nonuniformWitnesses ε s t).2 ⊆ t

theorem SimpleGraph.right_nonuniformWitnesses_card {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s 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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s 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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] (ε : 𝕜) (s 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.

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

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

theorem SimpleGraph.nonuniformWitness_spec {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s 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} [Field 𝕜] [LinearOrder 𝕜] [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.

@[simp]

theorem Finpartition.mk_mem_sparsePairs {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (u 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} [Field 𝕜] [LinearOrder 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [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.

@[simp]

theorem Finpartition.mk_mem_nonUniforms {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {u 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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DecidableEq α] {A : Finset α} (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} (hε : 0 < ε) : ⊥.nonUniforms G ε = ∅

def Finpartition.IsUniform {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [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 ε.

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

theorem Finpartition.isUniform_one {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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.

theorem Finpartition.card_nonuniformWitnesses_le {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} : (P.nonuniformWitnesses G ε s).card ≤ {t ∈ P.parts | s ≠ t ∧ ¬G.IsUniform ε s t}.card

theorem Finpartition.nonuniformWitness_mem_nonuniformWitnesses {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s 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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [Field 𝕜] [LinearOrder 𝕜] [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 δ.

@[simp]

theorem SimpleGraph.regularityReduced_adj {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (ε δ : 𝕜) (a b : α) : (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))

@[implicit_reducible]

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

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

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

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

theorem SimpleGraph.unreduced_edges_subset {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} : {x ∈ A ×ˢ A | match x with | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y} ⊆ ((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