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

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

• One or more equations did not get rendered due to their size.

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

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

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

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

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

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

theorem SimpleGraph.not_isUniform_iff {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} : ¬SimpleGraph.IsUniform G ε s t ↔ ∃ s' ⊆ s, ∃ t' ⊆ t, ↑s.card * ε ≤ ↑s'.card ∧ ↑t.card * ε ≤ ↑t'.card ∧ ε ≤ ↑|SimpleGraph.edgeDensity G s' t' - SimpleGraph.edgeDensity G 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

• SimpleGraph.nonuniformWitnesses G ε s t = if h : ¬SimpleGraph.IsUniform G ε s t then (Exists.choose ⋯, Exists.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 : ¬SimpleGraph.IsUniform G ε s t) : (SimpleGraph.nonuniformWitnesses G ε 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 : ¬SimpleGraph.IsUniform G ε s t) : ↑s.card * ε ≤ ↑(SimpleGraph.nonuniformWitnesses G ε 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 : ¬SimpleGraph.IsUniform G ε s t) : (SimpleGraph.nonuniformWitnesses G ε 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 : ¬SimpleGraph.IsUniform G ε s t) : ↑t.card * ε ≤ ↑(SimpleGraph.nonuniformWitnesses G ε 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 : ¬SimpleGraph.IsUniform G ε s t) : ε ≤ ↑|SimpleGraph.edgeDensity G (SimpleGraph.nonuniformWitnesses G ε s t).1 (SimpleGraph.nonuniformWitnesses G ε s t).2 - SimpleGraph.edgeDensity G 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

• SimpleGraph.nonuniformWitness G ε s t = if WellOrderingRel s t then (SimpleGraph.nonuniformWitnesses G ε s t).1 else (SimpleGraph.nonuniformWitnesses G ε t s).2

theorem SimpleGraph.nonuniformWitness_subset {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : 𝕜} {s : Finset α} {t : Finset α} (h : ¬SimpleGraph.IsUniform G ε s t) : SimpleGraph.nonuniformWitness G ε 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 : ¬SimpleGraph.IsUniform G ε s t) : ↑s.card * ε ≤ ↑(SimpleGraph.nonuniformWitness G ε 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₂ : ¬SimpleGraph.IsUniform G ε s t) : ε ≤ ↑|SimpleGraph.edgeDensity G (SimpleGraph.nonuniformWitness G ε s t) (SimpleGraph.nonuniformWitness G ε t s) - SimpleGraph.edgeDensity G s t|

Uniform partitions

noncomputable 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

• Finpartition.nonUniforms P G ε = Finset.filter (fun (uv : Finset α × Finset α) => ¬SimpleGraph.IsUniform G ε uv.1 uv.2) (Finset.offDiag P.parts)

theorem Finpartition.mk_mem_nonUniforms_iff {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (u : Finset α) (v : Finset α) (ε : 𝕜) : (u, v) ∈ Finpartition.nonUniforms P G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬SimpleGraph.IsUniform G ε 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 : ε ≤ ε') : Finpartition.nonUniforms P G ε' ⊆ Finpartition.nonUniforms P G ε

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

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

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

theorem Finpartition.isUniformOne {α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] : Finpartition.IsUniform P 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 : Finpartition.IsUniform P G ε) (h : ε ≤ ε') : Finpartition.IsUniform P 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 = ∅) : Finpartition.IsUniform P 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 : ¬Finpartition.IsUniform P 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

• Finpartition.nonuniformWitnesses P G ε s = Finset.image (SimpleGraph.nonuniformWitness G ε s) (Finset.filter (fun (t : Finset α) => s ≠ t ∧ ¬SimpleGraph.IsUniform G ε 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 : ¬SimpleGraph.IsUniform G ε s t) (ht : t ∈ P.parts) (hst : s ≠ t) : SimpleGraph.nonuniformWitness G ε s t ∈ Finpartition.nonuniformWitnesses P G ε s