Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax18.SzemerediRegularityLemma

Szemerédi's regularity lemma

concepts/Lax18/SzemerediRegularityLemma.lean · lax-18

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    Szemerédi's regularity lemma says that for every ε>0\varepsilon>0 and every positive lower bound m0m_0, there is an upper bound M≥m0M\ge m_0 such that every finite simple graph on at least m0m_0 vertices has an equitable ε\varepsilon-regular partition into kk parts with m0≤k≤Mm_0\le k\le M.

    The partition is clean: its parts are nonempty, pairwise disjoint, cover all vertices, and have sizes differing by at most one. There is no exceptional leftover class.

    Lean source view on GitHub

    1import Lax18.EnergyIncrement
    2import Lax18.EquitableCleanup
    3import Lax18.PartitionEnergyBounds
    4import Lax18.PartitionEnergyMonotonicity
    5
    6/-!
    7---
    8title: Szemerédi's regularity lemma
    9type: theorem
    10---
    11Szemerédi's regularity lemma says that for every \(\varepsilon>0\) and every
    12positive lower bound \(m_0\), there is an upper bound \(M\ge m_0\) such that
    13every finite simple graph on at least \(m_0\) vertices has an equitable
    14\(\varepsilon\)-regular partition into \(k\) parts with \(m_0\le k\le M\).
    15
    16The partition is clean: its parts are nonempty, pairwise disjoint, cover all
    17vertices, and have sizes differing by at most one. There is no exceptional
    18leftover class.
    19
    20# Source
    21The classical lower-bound statement and its energy-increment presentation
    22follow Reinhard Diestel, *Graph Theory*, 5th edition, Section 7.4. Diestel
    23uses an exceptional class to make the remaining classes exactly equal; the
    24statement here uses the equivalent clean equipartition convention, with all
    25part sizes differing by at most one.
    26-/
    27
    28namespace Lax18.SzemerediRegularityLemma
    29
    30open Lax18.FiniteGraphPartitions
    31open Lax18.RegularPartitions
    32
    33universe u
    34
    35/-- Szemerédi's regularity lemma for finite simple graphs, in the standard
    36lower-bound form. -/
    37axiom szemeredi_regularity_lemma :
    38 ∀ (ε : ℝ) (m₀ : ℕ),
    39 0 < ε →
    40 0 < m₀ →
    41 ∃ M : ℕ,
    42 m₀ ≤ M ∧
    43 ∀ {V : Type u} [Fintype V] [DecidableEq V]
    44 (G : SimpleGraph V),
    45 m₀ ≤ Fintype.card V →
    46 ∃ P : VertexPartition V,
    47 m₀ ≤ P.partCount ∧
    48 P.partCount ≤ M ∧
    49 IsEquitableRegularPartition G ε P
    50
    51end Lax18.SzemerediRegularityLemma
    52
    Show Proof

    Source

    The classical lower-bound statement and its energy-increment presentation follow Reinhard Diestel, Graph Theory, 5th edition, Section 7.4. Diestel uses an exceptional class to make the remaining classes exactly equal; the statement here uses the equivalent clean equipartition convention, with all part sizes differing by at most one.

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…