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

Lax18.RegularPairs

Regular pairs

concepts/Lax18/RegularPairs.lean · lax-18

definition

Loading review…

Sign in with ORCID

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

    Definition

    An ε\varepsilon-regular pair in a finite simple graph is a pair of nonempty vertex sets A,BA,B such that every XAX\subseteq A and YBY\subseteq B with XεA|X|\ge \varepsilon |A| and YεB|Y|\ge \varepsilon |B| has density within ε\varepsilon of the density of A,BA,B.

    This is the standard textbook definition, stated with real-valued densities. The definition itself does not require AA and BB to be disjoint; in the regularity lemma they are used as distinct blocks of a vertex partition, hence are disjoint there.

    Lean source view on GitHub

    1import Lax18.EdgeDensity
    2
    3/-!
    4---
    5title: Regular pairs
    6type: definition
    7---
    8An \(\varepsilon\)-regular pair in a finite simple graph is a pair of nonempty
    9vertex sets \(A,B\) such that every \(X\subseteq A\) and \(Y\subseteq B\) with
    10\(|X|\ge \varepsilon |A|\) and \(|Y|\ge \varepsilon |B|\) has density within
    11\(\varepsilon\) of the density of \(A,B\).
    12
    13This is the standard textbook definition, stated with real-valued densities.
    14The definition itself does not require \(A\) and \(B\) to be disjoint; in the
    15regularity lemma they are used as distinct blocks of a vertex partition, hence
    16are disjoint there.
    17-/
    18
    19namespace Lax18.RegularPairs
    20
    21open Lax18.EdgeDensity
    22
    23universe u
    24
    25variable {V : Type u} [Fintype V] [DecidableEq V]
    26
    27/-- `X` is a large enough subset of `A` for the threshold `ε`. -/
    28def LargeSubset (ε : ℝ) (A X : Finset V) : Prop :=
    29 X ⊆ A ∧ ε * (A.card : ℝ) ≤ (X.card : ℝ)
    30
    31/-- The pair `(A,B)` is `ε`-regular in `G`. -/
    32def IsRegularPair (G : SimpleGraph V) (ε : ℝ) (A B : Finset V) : Prop :=
    33 A.Nonempty ∧ B.Nonempty ∧
    34 ∀ X Y : Finset V,
    35 LargeSubset ε A X →
    36 LargeSubset ε B Y →
    37 |density G X Y - density G A B| ≤ ε
    38
    39end Lax18.RegularPairs
    40

    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…