Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Graph.Support

Supports of finite families of edges #

Adding an edge introduces zero, one, or two new endpoints. These exact cardinality increments are the combinatorial accounting used by the joint-message entropy bound.

source
def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.support {V : Type u_1} {E : Type u_2} [DecidableEq V] (left right : E → V) (edges : Finset E) :
Finset V

The vertices occurring among a finite family of edges.

Equations
Instances For
    source
    @[simp]
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.mem_support {V : Type u_1} {E : Type u_2} [DecidableEq V] (left right : E → V) (edges : Finset E) (v : V) :
    v ∈ support left right edges ↔ ∃ e ∈ edges, v = left e ∨ v = right e

    Membership in the support gives an incident edge in the selected family.

    source
    @[simp]
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.support_empty {V : Type u_1} {E : Type u_2} [DecidableEq V] (left right : E → V) :
    support left right ∅ = ∅

    The empty edge family has empty support.

    source
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.support_insert {V : Type u_1} {E : Type u_2} [DecidableEq V] [DecidableEq E] (left right : E → V) (edges : Finset E) (e : E) :
    support left right (insert e edges) = insert (left e) (insert (right e) (support left right edges))

    Inserting an edge adds precisely its two endpoints to the support.

    source
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.card_support_insert_of_mem_mem {V : Type u_1} {E : Type u_2} [DecidableEq V] [DecidableEq E] (left right : E → V) (edges : Finset E) (e : E) (hl : left e ∈ support left right edges) (hr : right e ∈ support left right edges) :
    (support left right (insert e edges)).card = (support left right edges).card

    No support vertex is added when both endpoints already occur.

    source
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.card_support_insert_of_mem_notMem {V : Type u_1} {E : Type u_2} [DecidableEq V] [DecidableEq E] (left right : E → V) (edges : Finset E) (e : E) (hl : left e ∈ support left right edges) (hr : right e ∉ support left right edges) :
    (support left right (insert e edges)).card = (support left right edges).card + 1

    Exactly one support vertex is added when only the right endpoint is new.

    source
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.card_support_insert_of_notMem_mem {V : Type u_1} {E : Type u_2} [DecidableEq V] [DecidableEq E] (left right : E → V) (edges : Finset E) (e : E) (hl : left e ∉ support left right edges) (hr : right e ∈ support left right edges) :
    (support left right (insert e edges)).card = (support left right edges).card + 1

    Exactly one support vertex is added when only the left endpoint is new.

    source
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.card_support_insert_of_notMem_notMem {V : Type u_1} {E : Type u_2} [DecidableEq V] [DecidableEq E] (left right : E → V) (edges : Finset E) (e : E) (hne : left e ≠ right e) (hl : left e ∉ support left right edges) (hr : right e ∉ support left right edges) :
    (support left right (insert e edges)).card = (support left right edges).card + 2

    Two support vertices are added when the distinct endpoints are both new.