# Numerical bounds for Szemerédi Regularity Lemma #

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 #

• SzemerediRegularity.stepBound: During the inductive step, a partition of size n is blown to size at most stepBound n.
• SzemerediRegularity.initialBound: The size of the partition we start the induction with.
• SzemerediRegularity.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][srl_itp]

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 stepBound n.

Equations
Instances For
theorem SzemerediRegularity.stepBound_pos {n : } :
0 < n

Alias of the reverse direction of SzemerediRegularity.stepBound_pos_iff.

theorem SzemerediRegularity.coe_stepBound {α : Type u_1} [] (n : ) :
= n * 4 ^ n

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem SzemerediRegularity.m_pos {α : Type u_1} [] [] {P : Finpartition Finset.univ} [] (hPα : P.parts.card * 16 ^ P.parts.card ) :
theorem SzemerediRegularity.coe_m_add_one_pos {α : Type u_1} [] [] {P : Finpartition Finset.univ} :
0 < ( / SzemerediRegularity.stepBound P.parts.card) + 1
theorem SzemerediRegularity.one_le_m_coe {α : Type u_1} [] [] {P : Finpartition Finset.univ} [] (hPα : P.parts.card * 16 ^ P.parts.card ) :
1 ( / SzemerediRegularity.stepBound P.parts.card)
theorem SzemerediRegularity.eps_pow_five_pos {α : Type u_1} [] [] {P : Finpartition Finset.univ} {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
0 < ε ^ 5
theorem SzemerediRegularity.eps_pos {α : Type u_1} [] [] {P : Finpartition Finset.univ} {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
0 < ε
theorem SzemerediRegularity.hundred_div_ε_pow_five_le_m {α : Type u_1} [] [] {P : Finpartition Finset.univ} {ε : } [] (hPα : P.parts.card * 16 ^ P.parts.card ) (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
100 / ε ^ 5 ( / SzemerediRegularity.stepBound P.parts.card)
theorem SzemerediRegularity.hundred_le_m {α : Type u_1} [] [] {P : Finpartition Finset.univ} {ε : } [] (hPα : P.parts.card * 16 ^ P.parts.card ) (hPε : 100 4 ^ P.parts.card * ε ^ 5) (hε : ε 1) :
theorem SzemerediRegularity.a_add_one_le_four_pow_parts_card {α : Type u_1} [] [] {P : Finpartition Finset.univ} :
/ P.parts.card - / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + 1 4 ^ P.parts.card
theorem SzemerediRegularity.card_aux₁ {α : Type u_1} [] [] {P : Finpartition Finset.univ} {u : } (hucard : u.card = / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + ( / P.parts.card - / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card)) :
(4 ^ P.parts.card - ( / P.parts.card - / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card)) * ( / SzemerediRegularity.stepBound P.parts.card) + ( / P.parts.card - / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card) * ( / SzemerediRegularity.stepBound P.parts.card + 1) = u.card
theorem SzemerediRegularity.card_aux₂ {α : Type u_1} [] [] {P : Finpartition Finset.univ} {u : } (hP : P.IsEquipartition) (hu : u P.parts) (hucard : ¬u.card = / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + ( / P.parts.card - / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card)) :
(4 ^ P.parts.card - ( / P.parts.card - / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + 1)) * ( / SzemerediRegularity.stepBound P.parts.card) + ( / P.parts.card - / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + 1) * ( / SzemerediRegularity.stepBound P.parts.card + 1) = u.card
theorem SzemerediRegularity.pow_mul_m_le_card_part {α : Type u_1} [] [] {P : Finpartition Finset.univ} {u : } (hP : P.IsEquipartition) (hu : u P.parts) :
4 ^ P.parts.card * ( / SzemerediRegularity.stepBound P.parts.card) u.card
noncomputable def SzemerediRegularity.initialBound (ε : ) (l : ) :

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

Equations
Instances For
theorem SzemerediRegularity.hundred_lt_pow_initialBound_mul {ε : } (hε : 0 < ε) (l : ) :
100 < * ε ^ 5
noncomputable def SzemerediRegularity.bound (ε : ) (l : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem SzemerediRegularity.mul_sq_le_sum_sq {ι : Type u_2} {𝕜 : Type u_3} {s : } {t : } {x : 𝕜} (hst : s t) (f : ι𝕜) (hs : x ^ 2 ((is, f i) / s.card) ^ 2) (hs' : s.card 0) :
s.card * x ^ 2 it, f i ^ 2
theorem SzemerediRegularity.add_div_le_sum_sq_div_card {ι : Type u_2} {𝕜 : Type u_3} {s : } {t : } {x : 𝕜} (hst : s t) (f : ι𝕜) (d : 𝕜) (hx : 0 x) (hs : x |(is, f i) / s.card - (it, f i) / t.card|) (ht : d ((it, f i) / t.card) ^ 2) :
d + s.card / t.card * x ^ 2 (it, f i ^ 2) / t.card

Extension for the positivity tactic: SzemerediRegularity.initialBound is always positive.

Instances For

Extension for the positivity tactic: SzemerediRegularity.bound is always positive.

Instances For