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 #

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

source

def szemeredi_regularity.step_bound (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 step_bound n.

Equations

szemeredi_regularity.step_bound n = n * 4 ^ n

source

theorem szemeredi_regularity.le_step_bound :

id ≤ szemeredi_regularity.step_bound

source

theorem szemeredi_regularity.step_bound_mono :

monotone szemeredi_regularity.step_bound

source

theorem szemeredi_regularity.step_bound_pos_iff {n : ℕ} :

0 < szemeredi_regularity.step_bound n ↔ 0 < n

source

theorem szemeredi_regularity.step_bound_pos {n : ℕ} :

0 < n → 0 < szemeredi_regularity.step_bound n

Alias of the reverse direction of szemeredi_regularity.step_bound_pos_iff.

source

meta def tactic.positivity_szemeredi_regularity :

expr → tactic tactic.positivity.strictness

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

source

theorem szemeredi_regularity.m_pos {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} [nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ≤ fintype.card α) :

0 < fintype.card α / szemeredi_regularity.step_bound P.parts.card

source

theorem szemeredi_regularity.coe_m_add_one_pos {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} :

0 < ↑(fintype.card α / szemeredi_regularity.step_bound P.parts.card) + 1

source

theorem szemeredi_regularity.one_le_m_coe {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} [nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ≤ fintype.card α) :

1 ≤ ↑(fintype.card α / szemeredi_regularity.step_bound P.parts.card)

source

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

source

theorem szemeredi_regularity.eps_pos {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} {ε : ℝ} (hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5) :

0 < ε

source

theorem szemeredi_regularity.hundred_div_ε_pow_five_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) :

100 / ε ^ 5 ≤ ↑(fintype.card α / szemeredi_regularity.step_bound P.parts.card)

source

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) :

100 ≤ fintype.card α / szemeredi_regularity.step_bound P.parts.card

source

theorem szemeredi_regularity.a_add_one_le_four_pow_parts_card {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} :

fintype.card α / P.parts.card - fintype.card α / szemeredi_regularity.step_bound P.parts.card * 4 ^ P.parts.card + 1 ≤ 4 ^ P.parts.card

source

theorem szemeredi_regularity.card_aux₁ {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} {u : finset α} (hucard : u.card = fintype.card α / szemeredi_regularity.step_bound P.parts.card * 4 ^ P.parts.card + (fintype.card α / P.parts.card - fintype.card α / szemeredi_regularity.step_bound P.parts.card * 4 ^ P.parts.card)) :

(4 ^ P.parts.card - (fintype.card α / P.parts.card - fintype.card α / szemeredi_regularity.step_bound P.parts.card * 4 ^ P.parts.card)) * (fintype.card α / szemeredi_regularity.step_bound P.parts.card) + (fintype.card α / P.parts.card - fintype.card α / szemeredi_regularity.step_bound P.parts.card * 4 ^ P.parts.card) * (fintype.card α / szemeredi_regularity.step_bound P.parts.card + 1) = u.card

source

theorem szemeredi_regularity.card_aux₂ {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} {u : finset α} (hP : P.is_equipartition) (hu : u ∈ P.parts) (hucard : ¬u.card = fintype.card α / szemeredi_regularity.step_bound P.parts.card * 4 ^ P.parts.card + (fintype.card α / P.parts.card - fintype.card α / szemeredi_regularity.step_bound P.parts.card * 4 ^ P.parts.card)) :

(4 ^ P.parts.card - (fintype.card α / P.parts.card - fintype.card α / szemeredi_regularity.step_bound P.parts.card * 4 ^ P.parts.card + 1)) * (fintype.card α / szemeredi_regularity.step_bound P.parts.card) + (fintype.card α / P.parts.card - fintype.card α / szemeredi_regularity.step_bound P.parts.card * 4 ^ P.parts.card + 1) * (fintype.card α / szemeredi_regularity.step_bound P.parts.card + 1) = u.card

source

theorem szemeredi_regularity.pow_mul_m_le_card_part {α : Type u_1} [decidable_eq α] [fintype α] {P : finpartition finset.univ} {u : finset α} (hP : P.is_equipartition) (hu : u ∈ P.parts) :

4 ^ P.parts.card * ↑(fintype.card α / szemeredi_regularity.step_bound P.parts.card) ≤ ↑(u.card)

source

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

szemeredi_regularity.initial_bound ε l = linear_order.max 7 (linear_order.max l (⌊real.log (100 / ε ^ 5) / real.log 4⌋₊ + 1))

source

theorem szemeredi_regularity.le_initial_bound (ε : ℝ) (l : ℕ) :

l ≤ szemeredi_regularity.initial_bound ε l

source

theorem szemeredi_regularity.seven_le_initial_bound (ε : ℝ) (l : ℕ) :

7 ≤ szemeredi_regularity.initial_bound ε l

source

theorem szemeredi_regularity.initial_bound_pos (ε : ℝ) (l : ℕ) :

0 < szemeredi_regularity.initial_bound ε l

source

theorem szemeredi_regularity.hundred_lt_pow_initial_bound_mul {ε : ℝ} (hε : 0 < ε) (l : ℕ) :

100 < 4 ^ szemeredi_regularity.initial_bound ε l * ε ^ 5

source

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

szemeredi_regularity.bound ε l = szemeredi_regularity.step_bound ^[⌊4 / ε ^ 5⌋₊] (szemeredi_regularity.initial_bound ε l) * 16 ^ szemeredi_regularity.step_bound ^[⌊4 / ε ^ 5⌋₊] (szemeredi_regularity.initial_bound ε l)

source

theorem szemeredi_regularity.initial_bound_le_bound (ε : ℝ) (l : ℕ) :

szemeredi_regularity.initial_bound ε l ≤ szemeredi_regularity.bound ε l

source

theorem szemeredi_regularity.le_bound (ε : ℝ) (l : ℕ) :

l ≤ szemeredi_regularity.bound ε l

source

theorem szemeredi_regularity.bound_pos (ε : ℝ) (l : ℕ) :

0 < szemeredi_regularity.bound ε l

source

theorem szemeredi_regularity.mul_sq_le_sum_sq {ι : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] {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)

source

theorem szemeredi_regularity.add_div_le_sum_sq_div_card {ι : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] {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)

source

meta def tactic.positivity_szemeredi_regularity_bound :

expr → tactic tactic.positivity.strictness

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