Documentation

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

Actual signed-edge weight bounds #

The local signed-conjunction certificates discharge the three cases of the edge-insertion induction. Enlarging the used support to the ambient vertex set then gives a bound stated only in terms of the numbers of edges and variables.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.Internal.weightBoundSelected {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq E] (edge : E → SignedEdge V) (selected : Finset E) :
WeightBound (tuple edge selected) (↑selected.card * edgeCost + ↑(support (fun (e : E) => (edge e).left) (fun (e : E) => (edge e).right) selected).card * vertexCost)

The actual local certificates give a weight for any selected edge message.

Equations
Instances For
    source
    noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.Internal.tupleUnivEquiv {E : Type u_2} [Fintype E] :
    (↥Finset.univ → Bool) ≃ (E → Bool)

    The tuple on all indices is equivalent to the ordinary function space.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.Internal.weightBound {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq E] [Fintype E] (edge : E → SignedEdge V) :
      WeightBound (fun (x : V → Bool) (e : E) => (edge e).eval x) (↑(Fintype.card E) * edgeCost + ↑(Fintype.card V) * vertexCost)

      The full edge message has the asserted cost in the ambient number of variables.

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