Documentation

Mathlib.Combinatorics.SimpleGraph.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.

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

Main declarations #

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

Alias of the reverse direction of SzemerediRegularity.stepBound_pos_iff.

theorem SzemerediRegularity.coe_stepBound {α : Type u_1} [Semiring α] (n : ) :
(stepBound 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
theorem SzemerediRegularity.eps_pow_five_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
0 < ε ^ 5
theorem SzemerediRegularity.eps_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
0 < ε
theorem SzemerediRegularity.hundred_div_ε_pow_five_le_m {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card Fintype.card α) (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
100 / ε ^ 5 ↑(Fintype.card α / stepBound P.parts.card)
theorem SzemerediRegularity.hundred_le_m {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card Fintype.card α) (hPε : 100 4 ^ P.parts.card * ε ^ 5) ( : ε 1) :
noncomputable def SzemerediRegularity.initialBound (ε : ) (l : ) :

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

Equations
theorem SzemerediRegularity.hundred_lt_pow_initialBound_mul {ε : } ( : 0 < ε) (l : ) :
100 < 4 ^ initialBound ε l * ε ^ 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.
theorem SzemerediRegularity.le_bound (ε : ) (l : ) :
l bound ε l
theorem SzemerediRegularity.bound_pos (ε : ) (l : ) :
0 < bound ε l
theorem SzemerediRegularity.mul_sq_le_sum_sq {ι : Type u_2} {𝕜 : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s t : Finset ι} {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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s t : Finset ι} {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