mathlib3 documentation

combinatorics.simple_graph.regularity.bound

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 #

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)