Lax Lean Archive

Edge Expansion and Subcubic Graphs

Lax920634.EdgeExpansion · concepts/Lax920634/EdgeExpansion.lean · lax-920634

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.

    Natural Language Statement

    Definition

    The edge boundary of a vertex set SS consists of the edges with one endpoint in SS and one outside. A finite graph has edge expansion at least hh if ∣∂S∣≥h∣S∣|\partial S|\ge h|S| whenever ∣S∣≤∣V∣/2|S|\le |V|/2. A graph is subcubic if every vertex has at most three neighbors.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Finite
    2import Mathlib.Data.Set.Card
    3import Mathlib.Data.Rat.Defs
    4
    5/-!
    6---
    7title: Edge Expansion and Subcubic Graphs
    8type: definition
    9---
    10The edge boundary of a vertex set SS consists of the edges with one endpoint
    11in SS and one outside. A finite graph has edge expansion at least hh if
    12∣∂S∣≥h∣S∣|\partial S|\ge h|S| whenever ∣S∣≤∣V∣/2|S|\le |V|/2. A graph is subcubic if
    13every vertex has at most three neighbors.
    14
    15# Formalization notes
    16
    17Boundary edges are represented by ordered pairs with the first endpoint in
    18SS and the second outside, so each undirected boundary edge is counted once.
    19`Set.ncard` avoids imposing decidability on mathematical predicates; every
    20set counted here is finite. Expansion constants are rational numbers.
    21-/
    22
    23namespace Lax920634.EdgeExpansion
    24
    25/-- Boundary edges oriented from the set to its complement, each counted once. -/
    26def edgeBoundary {V : Type} (G : SimpleGraph V) (S : Set V) : Set (V × V) :=
    27 {e | e.1 ∈ S ∧ e.2 ∉ S ∧ G.Adj e.1 e.2}
    28
    29/-- Every vertex set of size at most half the graph has at least `h` times
    30its size in boundary edges. -/
    31def HasEdgeExpansionAtLeast {V : Type} [Fintype V]
    32 (G : SimpleGraph V) (h : ℚ) : Prop :=
    33 ∀ S : Set V, 2 * S.ncard ≤ Fintype.card V →
    34 h * (S.ncard : ℚ) ≤ ((edgeBoundary G S).ncard : ℚ)
    35
    36/-- Every vertex has at most three distinct neighbors. -/
    37def IsSubcubic {V : Type} [Finite V] (G : SimpleGraph V) : Prop :=
    38 ∀ v, (G.neighborSet v).ncard ≤ 3
    39
    40end Lax920634.EdgeExpansion
    41
    Formalization notes

    Boundary edges are represented by ordered pairs with the first endpoint in SS and the second outside, so each undirected boundary edge is counted once. Set.ncardSet.ncard avoids imposing decidability on mathematical predicates; every set counted here is finite. Expansion constants are rational numbers.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…