Documentation

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

Signs of the edge and vertex entropy costs #

The logarithmic inequalities used here reduce to small integer comparisons.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.binEntropy_quarter :
Real.binEntropy (1 / 4) = 2 * Real.log 2 - 3 / 4 * Real.log 3

The quarter-biased entropy expanded into logarithms of integers.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.edgeCost_nonneg :
0 ≤ edgeCost

The per-edge cost is nonnegative.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.vertexCost_nonneg :
0 ≤ vertexCost

The per-vertex cost is nonnegative because 3 ^ 3 ≤ 2 ^ 5.