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.

Equations
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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem SzemerediRegularity.m_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card Fintype.card α) :
      theorem SzemerediRegularity.coe_m_add_one_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} :
      theorem SzemerediRegularity.one_le_m_coe {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card Fintype.card α) :
      theorem SzemerediRegularity.eps_pow_five_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
      0 < ε ^ 5
      theorem SzemerediRegularity.eps_pos {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {ε : } (hPε : 100 4 ^ P.parts.card * ε ^ 5) :
      0 < ε
      theorem SzemerediRegularity.hundred_div_ε_pow_five_le_m {α : Type u_1} [DecidableEq α] [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 α / SzemerediRegularity.stepBound P.parts.card)
      theorem SzemerediRegularity.hundred_le_m {α : Type u_1} [DecidableEq α] [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 SzemerediRegularity.a_add_one_le_four_pow_parts_card {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} :
      Fintype.card α / P.parts.card - Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + 1 4 ^ P.parts.card
      theorem SzemerediRegularity.card_aux₁ {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {u : Finset α} (hucard : u.card = Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card)) :
      (4 ^ P.parts.card - (Fintype.card α / P.parts.card - Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card)) * (Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + (Fintype.card α / P.parts.card - Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card) * (Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1) = u.card
      theorem SzemerediRegularity.card_aux₂ {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {u : Finset α} (hP : P.IsEquipartition) (hu : u P.parts) (hucard : ¬u.card = Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card)) :
      (4 ^ P.parts.card - (Fintype.card α / P.parts.card - Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + 1)) * (Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + (Fintype.card α / P.parts.card - Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + 1) * (Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1) = u.card
      theorem SzemerediRegularity.pow_mul_m_le_card_part {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {u : Finset α} (hP : P.IsEquipartition) (hu : u P.parts) :
      4 ^ P.parts.card * (Fintype.card α / SzemerediRegularity.stepBound P.parts.card) u.card
      noncomputable def SzemerediRegularity.initialBound (ε : ) (l : ) :

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

      Equations
      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.

        Equations
        • One or more equations did not get rendered due to their size.
        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 ((is, f i) / s.card) ^ 2) (hs' : s.card 0) :
          s.card * x ^ 2 it, 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 |(is, f i) / s.card - (it, f i) / t.card|) (ht : d ((it, f i) / t.card) ^ 2) :
          d + s.card / t.card * x ^ 2 (it, f i ^ 2) / t.card