Documentation

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

Joint entropy of signed two-variable conjunctions #

For m signed conjunctions on v independent Boolean coordinates, the joint message has a normalized weight of average natural-log cost at most m * (3/2 * log 2 - H(1/4)) + v * (H(1/4) - 3/4 * log 2). Here H is binary entropy with natural logarithms. The weight certificate implies the usual Shannon-entropy bound and applies directly to finite-fibre counting. Parallel edges, arbitrary signs, and every finite primary-support graph are allowed.

source
noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.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)

A joint weight for selected edges, charging only primary coordinates actually used.

Equations
Instances For
    source
    noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.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 graph entropy bound. Joint signed-conjunction messages cost at most m (3/2 log 2 - H(1/4)) + v (H(1/4) - 3/4 log 2) on v independent uniform bits.

    Equations
    Instances For
      source
      theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.input_le_cost_of_fibres {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq E] [Fintype E] (edge : E → SignedEdge V) {K : ℕ} (hK : 0 < K) (fibres : ∀ (message : E → Bool), {x : V → Bool | (fun (e : E) => (edge e).eval x) = message}.card ≤ K) :
      ↑(Fintype.card V) * Real.log 2 ≤ Real.log ↑K + ↑(Fintype.card E) * edgeCost + ↑(Fintype.card V) * vertexCost

      If no edge-message fibre has more than K inputs, the joint cost bounds the input count.