# mathlib3documentation

combinatorics.simple_graph.regularity.bound

# Numerical bounds for Szemerédi Regularity Lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file gathers the numerical facts required by the proof of Szemerédi's regularity lemma.

This entire file is internal to the proof of Szemerédi Regularity Lemma.

## Main declarations #

• szemeredi_regularity.step_bound: During the inductive step, a partition of size n is blown to size at most step_bound n.
• szemeredi_regularity.initial_bound: The size of the partition we start the induction with.
• szemeredi_regularity.bound: The upper bound on the size of the partition produced by our version of Szemerédi's regularity lemma.

## References #

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

Auxiliary function for Szemerédi's regularity lemma. Blowing up a partition of size n during the induction results in a partition of size at most step_bound n.

Equations

Alias of the reverse direction of szemeredi_regularity.step_bound_pos_iff.

Local extension for the positivity tactic: A few facts that are needed many times for the proof of Szemerédi's regularity lemma.

theorem szemeredi_regularity.m_pos {α : Type u_1} [decidable_eq α] [fintype α] [nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ) :
theorem szemeredi_regularity.one_le_m_coe {α : Type u_1} [decidable_eq α] [fintype α] [nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ) :
theorem szemeredi_regularity.eps_pow_five_pos {α : Type u_1} [decidable_eq α] [fintype α] {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
0 < ε ^ 5
theorem szemeredi_regularity.eps_pos {α : Type u_1} [decidable_eq α] [fintype α] {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
0 < ε
theorem szemeredi_regularity.hundred_div_ε_pow_five_le_m {α : Type u_1} [decidable_eq α] [fintype α] {ε : } [nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ) (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
100 / ε ^ 5
theorem szemeredi_regularity.hundred_le_m {α : Type u_1} [decidable_eq α] [fintype α] {ε : } [nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ) (hPε : 100 4 ^ P.parts.card * ε ^ 5) (hε : ε 1) :
theorem szemeredi_regularity.card_aux₁ {α : Type u_1} [decidable_eq α] [fintype α] {u : finset α} (hucard : u.card = + / P.parts.card - ) :
(4 ^ P.parts.card - / P.parts.card - * 4 ^ P.parts.card)) * + / P.parts.card - * = u.card
theorem szemeredi_regularity.card_aux₂ {α : Type u_1} [decidable_eq α] [fintype α] {u : finset α} (hP : P.is_equipartition) (hu : u P.parts) (hucard : ¬u.card = + / P.parts.card - ) :
(4 ^ P.parts.card - / P.parts.card - + 1)) * + / P.parts.card - + 1) * = u.card
theorem szemeredi_regularity.pow_mul_m_le_card_part {α : Type u_1} [decidable_eq α] [fintype α] {u : finset α} (hP : P.is_equipartition) (hu : u P.parts) :
noncomputable def szemeredi_regularity.initial_bound (ε : ) (l : ) :

Auxiliary function for Szemerédi's regularity lemma. The size of the partition by which we start blowing.

Equations
theorem szemeredi_regularity.hundred_lt_pow_initial_bound_mul {ε : } (hε : 0 < ε) (l : ) :
100 < * ε ^ 5
noncomputable def szemeredi_regularity.bound (ε : ) (l : ) :

An explicit bound on the size of the equipartition whose existence is given by Szemerédi's regularity lemma.

Equations
theorem szemeredi_regularity.le_bound (ε : ) (l : ) :
theorem szemeredi_regularity.bound_pos (ε : ) (l : ) :
theorem szemeredi_regularity.mul_sq_le_sum_sq {ι : Type u_2} {𝕜 : Type u_3} {s t : finset ι} {x : 𝕜} (hst : s t) (f : ι 𝕜) (hs : x ^ 2 (s.sum (λ (i : ι), f i) / (s.card)) ^ 2) (hs' : (s.card) 0) :
(s.card) * x ^ 2 t.sum (λ (i : ι), f i ^ 2)
theorem szemeredi_regularity.add_div_le_sum_sq_div_card {ι : Type u_2} {𝕜 : Type u_3} {s t : finset ι} {x : 𝕜} (hst : s t) (f : ι 𝕜) (d : 𝕜) (hx : 0 x) (hs : x |s.sum (λ (i : ι), f i) / (s.card) - t.sum (λ (i : ι), f i) / (t.card)|) (ht : d (t.sum (λ (i : ι), f i) / (t.card)) ^ 2) :
d + (s.card) / (t.card) * x ^ 2 t.sum (λ (i : ι), f i ^ 2) / (t.card)

Extension for the positivity tactic: szemeredi_regularity.initial_bound and szemeredi_regularity.bound are always positive.