Numerical bounds for Szemerédi Regularity Lemma #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 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.
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) :