mathlib documentation

combinatorics.simple_graph.regularity.bound

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 #

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

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

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