Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Graph.Internal.Insert

Extending an edge message by one coordinate #

The inserted coordinate is equivalent to a pair of its Boolean value and the old message. This equivalence lets a normalized conditional kernel extend the old weight.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.tupleInsertEquiv {E : Type u_2} [DecidableEq E] (selected : Finset E) (e : E) (fresh : e ∉ selected) :
Bool × (↥selected → Bool) ≃ (↥(insert e selected) → Bool)

A new Boolean coordinate together with an old tuple is the tuple on an insertion.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.tupleInsertEquiv_apply {V : Type u_1} {E : Type u_2} [DecidableEq E] (edge : E → SignedEdge V) (selected : Finset E) (e : E) (fresh : e ∉ selected) (x : V → Bool) :
    (tupleInsertEquiv selected e fresh) ((edge e).eval x, tuple edge selected x) = tuple edge (insert e selected) x

    The insertion equivalence combines the actual edge value and actual previous tuple.

    source
    noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.insertWeight {V : Type u_1} {E : Type u_2} [DecidableEq V] [DecidableEq E] [Fintype V] (edge : E → SignedEdge V) (selected : Finset E) (e : E) (fresh : e ∉ selected) {a b : ℝ} (previous : WeightBound (tuple edge selected) a) (next : ConditionalWeightBound (edge e).eval (tuple edge selected) b) :
    WeightBound (tuple edge (insert e selected)) (a + b)

    An old tuple weight and one conditional edge weight extend to the inserted tuple.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For