Lax Lean Archive

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

Lax18.RegularPartitions

Regular partitions

concepts/Lax18/RegularPartitions.lean · lax-18

definition

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

    Definition

    For a vertex partition with kk parts, an unordered pair of distinct parts is irregular if it is not an ε\varepsilon-regular pair. A partition is ε\varepsilon-regular when the number of irregular unordered pairs is at most εk2\varepsilon k^2.

    An equitable ε\varepsilon-regular partition is an ε\varepsilon-regular partition whose part sizes differ by at most one.

    Lean source view on GitHub

    1import Lax18.FiniteGraphPartitions
    2import Lax18.RegularPairs
    3
    4/-!
    5---
    6title: Regular partitions
    7type: definition
    8---
    9For a vertex partition with \(k\) parts, an unordered pair of distinct parts is
    10irregular if it is not an \(\varepsilon\)-regular pair. A partition is
    11\(\varepsilon\)-regular when the number of irregular unordered pairs is at most
    12\(\varepsilon k^2\).
    13
    14An equitable \(\varepsilon\)-regular partition is an \(\varepsilon\)-regular
    15partition whose part sizes differ by at most one.
    16-/
    17
    18namespace Lax18.RegularPartitions
    19
    20open Lax18.FiniteGraphPartitions
    21open Lax18.RegularPairs
    22
    23universe u
    24
    25variable {V : Type u} [Fintype V] [DecidableEq V]
    26
    27/-- The unordered irregular pairs of parts, represented by index pairs
    28`i < j`. -/
    29noncomputable def irregularPairIndices
    30 (G : SimpleGraph V) (ε : ℝ)
    31 (P : VertexPartition V) : Finset (Fin P.partCount × Fin P.partCount) := by
    32 classical
    33 exact
    34 (Finset.univ.product Finset.univ).filter
    35 (fun p : Fin P.partCount × Fin P.partCount =>
    36 p.1 < p.2 ∧
    37 ¬ IsRegularPair G ε (P.part p.1) (P.part p.2))
    38
    39/-- The number of unordered irregular pairs of parts. -/
    40noncomputable def irregularPairCount
    41 (G : SimpleGraph V) (ε : ℝ)
    42 (P : VertexPartition V) : ℕ :=
    43 (irregularPairIndices G ε P).card
    44
    45/-- A partition is `ε`-regular if it has at most `ε k^2` irregular unordered
    46pairs of distinct parts. -/
    47def IsRegularPartition (G : SimpleGraph V) (ε : ℝ)
    48 (P : VertexPartition V) : Prop :=
    49 (irregularPairCount G ε P : ℝ) ≤ ε * (P.partCount : ℝ) ^ 2
    50
    51/-- A clean equitable `ε`-regular partition. -/
    52def IsEquitableRegularPartition
    53 (G : SimpleGraph V) (ε : ℝ) (P : VertexPartition V) : Prop :=
    54 P.Equitable ∧ IsRegularPartition G ε P
    55
    56end Lax18.RegularPartitions
    57

    Builds on

    Used by

    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…