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]

def SzemerediRegularity.stepBound (n : ℕ) : ℕ

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.

theorem SzemerediRegularity.le_stepBound : id ≤ SzemerediRegularity.stepBound

theorem SzemerediRegularity.stepBound_mono : Monotone SzemerediRegularity.stepBound

theorem SzemerediRegularity.stepBound_pos_iff {n : ℕ} : 0 < SzemerediRegularity.stepBound n ↔ 0 < n

theorem SzemerediRegularity.stepBound_pos {n : ℕ} : 0 < n → 0 < SzemerediRegularity.stepBound n

Alias of the reverse direction of SzemerediRegularity.stepBound_pos_iff.

def SzemerediRegularity.Positivity.tacticSz_positivity : Lean.ParserDescr

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

theorem SzemerediRegularity.m_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} [Nonempty α] (hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α) : 0 < Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts)

theorem SzemerediRegularity.coe_m_add_one_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} : 0 < ↑(Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts)) + 1

theorem SzemerediRegularity.one_le_m_coe {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} [Nonempty α] (hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α) : 1 ≤ ↑(Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts))

theorem SzemerediRegularity.eps_pow_five_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : ℝ} (hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5) : 0 < ε ^ 5

theorem SzemerediRegularity.eps_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : ℝ} (hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5) : 0 < ε

theorem SzemerediRegularity.hundred_div_ε_pow_five_le_m {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : ℝ} [Nonempty α] (hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α) (hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5) : ↑100 / ε ^ 5 ≤ ↑(Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts))

theorem SzemerediRegularity.hundred_le_m {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : ℝ} [Nonempty α] (hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α) (hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5) (hε : ε ≤ 1) : 100 ≤ Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts)

theorem SzemerediRegularity.a_add_one_le_four_pow_parts_card {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} : Fintype.card α / Finset.card P.parts - Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts + 1 ≤ 4 ^ Finset.card P.parts

theorem SzemerediRegularity.card_aux₁ {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {u : Finset α} (hucard : Finset.card u = Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts + (Fintype.card α / Finset.card P.parts - Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts)) : (4 ^ Finset.card P.parts - (Fintype.card α / Finset.card P.parts - Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts)) * (Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts)) + (Fintype.card α / Finset.card P.parts - Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts) * (Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) + 1) = Finset.card u

theorem SzemerediRegularity.card_aux₂ {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {u : Finset α} (hP : Finpartition.IsEquipartition P) (hu : u ∈ P.parts) (hucard : ¬Finset.card u = Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts + (Fintype.card α / Finset.card P.parts - Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts)) : (4 ^ Finset.card P.parts - (Fintype.card α / Finset.card P.parts - Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts + 1)) * (Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts)) + (Fintype.card α / Finset.card P.parts - Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts + 1) * (Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts) + 1) = Finset.card u

theorem SzemerediRegularity.pow_mul_m_le_card_part {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {u : Finset α} (hP : Finpartition.IsEquipartition P) (hu : u ∈ P.parts) : 4 ^ Finset.card P.parts * ↑(Fintype.card α / SzemerediRegularity.stepBound (Finset.card P.parts)) ≤ ↑(Finset.card u)

noncomputable def SzemerediRegularity.initialBound (ε : ℝ) (l : ℕ) : ℕ

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

theorem SzemerediRegularity.le_initialBound (ε : ℝ) (l : ℕ) : l ≤ SzemerediRegularity.initialBound ε l

theorem SzemerediRegularity.seven_le_initialBound (ε : ℝ) (l : ℕ) : 7 ≤ SzemerediRegularity.initialBound ε l

theorem SzemerediRegularity.initialBound_pos (ε : ℝ) (l : ℕ) : 0 < SzemerediRegularity.initialBound ε l

theorem SzemerediRegularity.hundred_lt_pow_initialBound_mul {ε : ℝ} (hε : 0 < ε) (l : ℕ) : ↑100 < 4 ^ SzemerediRegularity.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.

theorem SzemerediRegularity.initialBound_le_bound (ε : ℝ) (l : ℕ) : SzemerediRegularity.initialBound ε l ≤ SzemerediRegularity.bound ε l

theorem SzemerediRegularity.le_bound (ε : ℝ) (l : ℕ) : l ≤ SzemerediRegularity.bound ε l

theorem SzemerediRegularity.bound_pos (ε : ℝ) (l : ℕ) : 0 < SzemerediRegularity.bound ε l

theorem SzemerediRegularity.mul_sq_le_sum_sq {ι : Type u_2} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {s : Finset ι} {t : Finset ι} {x : 𝕜} (hst : s ⊆ t) (f : ι → 𝕜) (hs : x ^ 2 ≤ ((Finset.sum s fun i => f i) / ↑(Finset.card s)) ^ 2) (hs' : ↑(Finset.card s) ≠ 0) : ↑(Finset.card s) * x ^ 2 ≤ Finset.sum t fun i => f i ^ 2

theorem SzemerediRegularity.add_div_le_sum_sq_div_card {ι : Type u_2} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {s : Finset ι} {t : Finset ι} {x : 𝕜} (hst : s ⊆ t) (f : ι → 𝕜) (d : 𝕜) (hx : 0 ≤ x) (hs : x ≤ |(Finset.sum s fun i => f i) / ↑(Finset.card s) - (Finset.sum t fun i => f i) / ↑(Finset.card t)|) (ht : d ≤ ((Finset.sum t fun i => f i) / ↑(Finset.card t)) ^ 2) : d + ↑(Finset.card s) / ↑(Finset.card t) * x ^ 2 ≤ (Finset.sum t fun i => f i ^ 2) / ↑(Finset.card t)

def Tactic.evalInitialBound : Mathlib.Meta.Positivity.PositivityExt

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

def Tactic.evalBound : Mathlib.Meta.Positivity.PositivityExt

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