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 sizen
is 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.
References #
Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean
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.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.
Equations
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) :