mathlib documentation

combinatorics.simple_graph.regularity.bound

Numerical bounds for Szemerédi Regularity Lemma #

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

Main declarations #

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
theorem szemeredi_regularity.eps_pow_five_pos {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
0 < ε ^ 5
theorem szemeredi_regularity.eps_pos {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
0 < ε
theorem szemeredi_regularity.hundred_le_m {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} {ε : } [nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card fintype.card α) (hPε : 100 4 ^ P.parts.card * ε ^ 5) (hε : ε 1) :
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
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