Regular pairs

Lax18.RegularPairs · 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.

    Natural Language Statement

    Definition

    An ε\varepsilon-regular pair in a finite simple graph is a pair of nonempty vertex sets A,BA,B such that every X⊆AX\subseteq A and Y⊆BY\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.

    Concept map
    2 concepts; 7 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    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
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…