Weight certificates from one-sided Boolean bias #
A Boolean message with true probability at most p ≤ 1/2 has a normalized
weight certificate of cost binEntropy p. No independence is required.
noncomputable def
Algebraic.Cutwidth.Aggregate.Geometry.Entropy.WeightBound.ofTrueCountLE
{X : Type u_1}
[Fintype X]
(bit : X → Bool)
{p : ℝ}
(positive : 0 < p)
(half : p ≤ 1 / 2)
(count : ↑{x : X | bit x = true}.card ≤ p * ↑(Fintype.card X))
:
WeightBound bit (Real.binEntropy p)
A one-sided bound on the number of true messages gives a binary-entropy cost.
Equations
- One or more equations did not get rendered due to their size.