Documentation

Mathlib.Combinatorics.SimpleGraph.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][srl_itp]

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 stepBound n.

Instances For

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

    Instances For
      theorem SzemerediRegularity.m_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} [Nonempty α] (hPα : Finset.card P.parts * 16 ^ Finset.card P.parts Fintype.card α) :
      theorem SzemerediRegularity.one_le_m_coe {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} [Nonempty α] (hPα : Finset.card P.parts * 16 ^ Finset.card P.parts Fintype.card α) :
      theorem SzemerediRegularity.eps_pow_five_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } (hPε : 100 4 ^ Finset.card P.parts * ε ^ 5) :
      0 < ε ^ 5
      theorem SzemerediRegularity.eps_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } (hPε : 100 4 ^ Finset.card P.parts * ε ^ 5) :
      0 < ε
      theorem SzemerediRegularity.hundred_div_ε_pow_five_le_m {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } [Nonempty α] (hPα : Finset.card P.parts * 16 ^ Finset.card P.parts Fintype.card α) (hPε : 100 4 ^ Finset.card P.parts * ε ^ 5) :
      theorem SzemerediRegularity.hundred_le_m {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } [Nonempty α] (hPα : Finset.card P.parts * 16 ^ Finset.card P.parts Fintype.card α) (hPε : 100 4 ^ Finset.card P.parts * ε ^ 5) (hε : ε 1) :
      theorem SzemerediRegularity.pow_mul_m_le_card_part {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {u : Finset α} (hP : Finpartition.IsEquipartition P) (hu : u P.parts) :
      noncomputable def SzemerediRegularity.initialBound (ε : ) (l : ) :

      Auxiliary function for Szemerédi's regularity lemma. The size of the partition by which we start blowing.

      Instances For
        noncomputable def SzemerediRegularity.bound (ε : ) (l : ) :

        An explicit bound on the size of the equipartition whose existence is given by Szemerédi's regularity lemma.

        Instances For
          theorem SzemerediRegularity.mul_sq_le_sum_sq {ι : Type u_2} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {s : Finset ι} {t : Finset ι} {x : 𝕜} (hst : s t) (f : ι𝕜) (hs : x ^ 2 ((Finset.sum s fun i => f i) / ↑(Finset.card s)) ^ 2) (hs' : ↑(Finset.card s) 0) :
          ↑(Finset.card s) * x ^ 2 Finset.sum t fun i => f i ^ 2
          theorem SzemerediRegularity.add_div_le_sum_sq_div_card {ι : Type u_2} {𝕜 : Type u_3} [LinearOrderedField 𝕜] {s : Finset ι} {t : Finset ι} {x : 𝕜} (hst : s t) (f : ι𝕜) (d : 𝕜) (hx : 0 x) (hs : x |(Finset.sum s fun i => f i) / ↑(Finset.card s) - (Finset.sum t fun i => f i) / ↑(Finset.card t)|) (ht : d ((Finset.sum t fun i => f i) / ↑(Finset.card t)) ^ 2) :
          d + ↑(Finset.card s) / ↑(Finset.card t) * x ^ 2 (Finset.sum t fun i => f i ^ 2) / ↑(Finset.card t)

          Extension for the positivity tactic: SzemerediRegularity.bound is always positive.

          Instances For