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 #
szemeredi_regularity.step_bound: During the inductive step, a partition of sizenis blown to size at moststep_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.
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
theorem
szemeredi_regularity.step_bound_pos_iff
{n : ℕ} :
0 < szemeredi_regularity.step_bound n ↔ 0 < n
Alias of the reverse direction of szemeredi_regularity.step_bound_pos_iff`.
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 α) :
theorem
szemeredi_regularity.m_coe_pos
{α : Type u_1}
[decidable_eq α]
[fintype α]
{P : finpartition finset.univ}
[nonempty α]
(hPα : P.parts.card * 16 ^ P.parts.card ≤ fintype.card α) :
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
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 α) :
theorem
szemeredi_regularity.eps_pow_five_pos
{α : Type u_1}
[decidable_eq α]
[fintype α]
{P : finpartition finset.univ}
{ε : ℝ}
(hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 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_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)
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) :
theorem
szemeredi_regularity.a_add_one_le_four_pow_parts_card
{α : Type u_1}
[decidable_eq α]
[fintype α]
{P : finpartition finset.univ} :
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
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
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) :
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))
theorem
szemeredi_regularity.hundred_lt_pow_initial_bound_mul
{ε : ℝ}
(hε : 0 < ε)
(l : ℕ) :
100 < 4 ^ szemeredi_regularity.initial_bound ε l * ε ^ 5
An explicit bound on the size of the equipartition whose existence is given by Szemerédi's regularity lemma.