Lax Lean Archive

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

Lax18.EdgeDensity

Edge density between two vertex sets

concepts/Lax18/EdgeDensity.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 finite simple graph, the edge count between two vertex sets counts the ordered cross-pairs (a,b)∈A×B(a,b)\in A\times B which are adjacent in the graph. When the two sets are disjoint, this counts each edge between them exactly once, in the direction from AA to BB.

    The edge density of AA and BB is this edge count divided by ∣A∣∣B∣|A||B|, as a real number. If one side is empty, the density is defined to be zero; regular pairs themselves require nonempty sides.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2import Mathlib.Data.Real.Basic
    3
    4/-!
    5---
    6title: Edge density between two vertex sets
    7type: definition
    8---
    9For a finite simple graph, the edge count between two vertex sets counts the
    10ordered cross-pairs \((a,b)\in A\times B\) which are adjacent in the graph.
    11When the two sets are disjoint, this counts each edge between them exactly
    12once, in the direction from \(A\) to \(B\).
    13
    14The edge density of \(A\) and \(B\) is this edge count divided by
    15\(|A||B|\), as a real number. If one side is empty, the density is defined to
    16be zero; regular pairs themselves require nonempty sides.
    17-/
    18
    19namespace Lax18.EdgeDensity
    20
    21universe u
    22
    23variable {V : Type u} [Fintype V] [DecidableEq V]
    24
    25/-- The number of adjacent ordered pairs from `A` to `B`. -/
    26noncomputable def edgeCountBetween (G : SimpleGraph V)
    27 (A B : Finset V) : ℕ := by
    28 classical
    29 exact ((A.product B).filter fun p : V × V => G.Adj p.1 p.2).card
    30
    31/-- The real-valued edge density between two vertex sets. -/
    32noncomputable def density (G : SimpleGraph V) (A B : Finset V) : ℝ :=
    33 if A.card = 0 ∨ B.card = 0 then
    34 0
    35 else
    36 (edgeCountBetween G A B : ℝ) / ((A.card : ℝ) * (B.card : ℝ))
    37
    38end Lax18.EdgeDensity
    39

    Builds on

    none

    Used by

    From Mathlib

    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…