Szemerédi regularity relative to a seed partition

Mathlib's szemeredi_regularity produces a uniform equipartition, but relates it to no prescribed partition. Refining its output afterwards does not help, since uniformity is not inherited by refinements, and a common refinement with a seed partition is not an equipartition in general. This file instead runs the energy-increment induction behind szemeredi_regularity from a given starting equipartition. Mathlib's SzemerediRegularity.increment is a Finpartition.bind, so it refines its input exactly, and each partition built by the induction refines the start.

Starting from an equipartition that almost refines a seed P₀ (provided by Finpartition.IsEquipartition.exists_equipartition_card_eq_almostRefines), this yields a uniform equipartition that still almost refines P₀, with a number of parts bounded in terms of ε and the number of parts of P₀ only. Starting instead from an exact refinement of an equipartition P into equally many pieces per part, it yields a uniform equipartition refining P exactly. Regularity statements that iterate the regularity lemma, such as strong regularity, need this control on the relation between successive partitions.

Main declarations

• SimpleGraph.szemeredi_regularity_le: a uniform equipartition refining a given equipartition with enough parts, of size bounded in terms of ε and the starting size.
• TauCeti.refiningRegularityBound: the complexity bound for almost-refining regularity.
• SimpleGraph.exists_regular_equipartition_almost_refining: a uniform equipartition almost refining a given equipartition P₀ up to ε, with at most refiningRegularityBound ε #P₀.parts parts.
• TauCeti.nestedRefinementBound: the complexity bound for exactly refining regularity.
• SimpleGraph.exists_regular_exact_refining_equipartition: a uniform equipartition refining a given equipartition P exactly, with at most nestedRefinementBound δ #P.parts parts.
• SimpleGraph.exists_regular_almostRefines_le_card: a uniform equipartition almost refining a given equipartition P₀ up to ε, with at least a requested number of parts.

References

The induction follows the proof of szemeredi_regularity in Mathlib, by Yaël Dillies and Bhavik Mehta.

• [Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean][srl_itp]

theorem SimpleGraph.szemeredi_regularity_le {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} {P₁ : Finpartition Finset.univ} (hP₁ : P₁.IsEquipartition) (hP₇ : 7 ≤ P₁.parts.card) (hPε : 100 ≤ 4 ^ P₁.parts.card * ε ^ 5) (hα : SzemerediRegularity.stepBound^[⌊4 / ε ^ 5⌋₊] P₁.parts.card * 16 ^ SzemerediRegularity.stepBound^[⌊4 / ε ^ 5⌋₊] P₁.parts.card ≤ Fintype.card α) : ∃ P ≤ P₁, P.IsEquipartition ∧ P.IsUniform G ε ∧ P.parts.card ≤ SzemerediRegularity.stepBound^[⌊4 / ε ^ 5⌋₊ + 1] P₁.parts.card

Szemerédi's regularity lemma below a starting equipartition. If P₁ is an equipartition with at least 7 parts and 100 ≤ 4 ^ #P₁.parts * ε ^ 5, and the graph is large enough, then some ε-uniform equipartition refines P₁ and has at most stepBound^[⌊4 / ε ^ 5⌋₊ + 1] #P₁.parts parts.

noncomputable def TauCeti.nestedRefinementBound (δ : ℝ) (l : ℕ) : ℕ

The complexity bound for exists_regular_exact_refining_equipartition: the bound of Szemerédi's regularity lemma started from initialBound δ 0 * l parts. It depends only on δ and the number l of parts of the partition being refined.

theorem TauCeti.nestedRefinementBound_def (δ : ℝ) (l : ℕ) : nestedRefinementBound δ l = SzemerediRegularity.bound δ (SzemerediRegularity.initialBound δ 0 * l)

The complexity bound is Szemerédi's bound started from initialBound δ 0 * l parts.

theorem TauCeti.le_nestedRefinementBound (δ : ℝ) (l : ℕ) : l ≤ nestedRefinementBound δ l

The complexity bound for exactly refining regularity is at least the number of parts being refined.

noncomputable def TauCeti.refiningRegularityBound (ε : ℝ) (l : ℕ) : ℕ

The complexity bound for exists_regular_equipartition_almost_refining: the bound of Szemerédi's regularity lemma with at least ⌈2 * l / ε⌉₊ initial parts. It depends only on ε and the number l of parts of the seed partition.

theorem TauCeti.refiningRegularityBound_def (ε : ℝ) (l : ℕ) : refiningRegularityBound ε l = SzemerediRegularity.bound ε ⌈2 * ↑l / ε⌉₊

The complexity bound is Szemerédi's bound with at least ⌈2 * l / ε⌉₊ initial parts.

theorem SimpleGraph.exists_regular_equipartition_almost_refining {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} (P₀ : Finpartition Finset.univ) (hP₀ : P₀.IsEquipartition) (hε : 0 < ε) : ∃ (P : Finpartition Finset.univ), P.IsEquipartition ∧ P.IsUniform G ε ∧ P.AlmostRefines P₀ ε ∧ P.parts.card ≤ TauCeti.refiningRegularityBound ε P₀.parts.card

Szemerédi's regularity lemma relative to a seed. Every equipartition P₀ of a finite graph is almost refined, up to ε, by an ε-uniform equipartition with at most refiningRegularityBound ε #P₀.parts parts.

theorem SimpleGraph.exists_regular_exact_refining_equipartition {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (hP : P.IsEquipartition) {δ : ℝ} (hδ : 0 < δ) : ∃ Q ≤ P, Q.IsEquipartition ∧ Q.IsUniform G δ ∧ Q.parts.card ≤ TauCeti.nestedRefinementBound δ P.parts.card

Szemerédi's regularity lemma refining an equipartition exactly. Every equipartition P of a finite graph is refined exactly by a δ-uniform equipartition with at most nestedRefinementBound δ #P.parts parts.

theorem SimpleGraph.exists_regular_almostRefines_le_card {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} (P₀ : Finpartition Finset.univ) (hP₀ : P₀.IsEquipartition) {l : ℕ} (hl : l ≤ Fintype.card α) (hε : 0 < ε) : ∃ (P : Finpartition Finset.univ), P.IsEquipartition ∧ P.IsUniform G ε ∧ P.AlmostRefines P₀ ε ∧ l ≤ P.parts.card ∧ P.parts.card ≤ TauCeti.nestedRefinementBound ε (max (max l P₀.parts.card) ⌈2 * ↑(max l P₀.parts.card) / ε⌉₊)

Szemerédi's regularity lemma relative to a seed, with a minimum number of parts. Every equipartition P₀ of a finite graph is almost refined, up to ε, by an ε-uniform equipartition with at least l parts, for any requested l ≤ card α. It is obtained by refining exactly an equipartition into max l₀ ⌈2 * l₀ / ε⌉₊ parts almost refining P₀, where l₀ = max l #P₀.parts, so it has at most nestedRefinementBound ε (max l₀ ⌈2 * l₀ / ε⌉₊) parts.