InformationTheory.Shannon.BoolLaw

Imports 3

The two-point law and the cost of a small mixing weight #

Mixing two laws with weight lam is carried by a law on Bool that records which of the two was drawn. Clamping the weight at 1 makes that law a probability measure for every weight, so the instance is available before any side condition is discharged, which is what lets the mixture be formed and its information slots be stated at all.

A variable that records the branch of such a mixture carries the binary entropy of the weight, and that is the price paid for mixing. Since the binary entropy vanishes at 0 together with the weight itself, the price can be pushed below any positive slack, simultaneously with a linear cost in the weight.

Main definitions #

boolLaw lam — the two-point law giving true the clamped weight lam ⊓ 1.

Main statements #

lintegral_boolLaw — an integral against the two-point law is the weighted sum of its two values.
entropy_eq_binEntropy_of_map_boolLaw — a variable distributed as the two-point law has the binary entropy of the weight.
exists_mul_add_binEntropy_lt — a positive weight below 1 whose linear cost and binary entropy stay under any positive slack, for two nonnegative coefficients at once.

The two-point law #

noncomputable def

InformationTheory.Shannon.boolLaw

source

(lam : ENNReal) :

MeasureTheory.Measure Bool

The two-point law with weight lam, clamped so that it is a probability measure for every weight. The clamp is what makes IsProbabilityMeasure an instance rather than a lemma with a side condition, and the conditional mutual information of a mixture along this law needs that instance in order to be stated at all.

Equations