Weighted counting of biased Boolean messages

A product distribution assigns probability one quarter to the rare outcome of each biased coordinate. Summing log x ≤ x - 1 proves the usual entropy bound directly, without assuming independence of the message coordinates.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.sum_log_le_of_sum_le {X : Type u_1} [Fintype X] (f : X → ℝ) (positive : ∀ (x : X), 0 < f x) {a : ℝ} (ha : 0 < a) (bound : ∑ x : X, f x ≤ ↑(Fintype.card X) * a) : ∑ x : X, Real.log (f x) ≤ ↑(Fintype.card X) * Real.log a

A finite logarithmic mean bound, derived from the tangent inequality for log.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.biasSaving : ℝ

The natural-log saving supplied by a coordinate whose rare value has probability at most 1/4.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.biasSaving = Real.log 2 - Real.binEntropy (1 / 4)

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitWeight (biased rare value : Bool) : ℝ

The probability assigned to one Boolean coordinate.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitWeight biased rare value = if biased = true then if value = rare then 1 / 4 else 3 / 4 else 1 / 2

@[simp]

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitWeight_pos (biased rare value : Bool) : 0 < bitWeight biased rare value

Every one-bit outcome receives strictly positive weight.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.sum_bitWeight (biased rare : Bool) : ∑ value : Bool, bitWeight biased rare value = 1

The weights on both one-bit outcomes sum to one.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.messageWeight {ι : Type u_1} [Fintype ι] (biased rare message : ι → Bool) : ℝ

Product weights on all the bits of a message.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.messageWeight biased rare message = ∏ i : ι, Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitWeight (biased i) (rare i) (message i)

@[simp]

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.messageWeight_pos {ι : Type u_1} [Fintype ι] (biased rare message : ι → Bool) : 0 < messageWeight biased rare message

Every full message receives strictly positive product weight.

@[simp]

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.sum_messageWeight {ι : Type u_1} [Fintype ι] (biased rare : ι → Bool) : ∑ message : ι → Bool, messageWeight biased rare message = 1

The product weights form a probability mass on the message cube.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.sum_weight_key_le {X : Type u_1} {T : Type u_2} [Fintype X] [Fintype T] (key : X → T) (weight : T → ℝ) (nonneg : ∀ (t : T), 0 ≤ weight t) (mass : ∑ t : T, weight t = 1) {K : ℕ} (fibres : ∀ (t : T), {x : X | key x = t}.card ≤ K) : ∑ x : X, weight (key x) ≤ ↑K

A key with fibres of size at most K pulls back a probability mass to mass at most K.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.biasSaving_pos : 0 < biasSaving

Bias gives a strictly positive saving over one unbiased bit.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.sum_log_bitWeight_ge {X : Type u_1} [Fintype X] (bit : X → Bool) (rare biased : Bool) (bias : biased = true → 4 * {x : X | bit x = rare}.card ≤ Fintype.card X) : (-↑(Fintype.card X) * Real.log 2 + if biased = true then ↑(Fintype.card X) * biasSaving else 0) ≤ ∑ x : X, Real.log (bitWeight biased rare (bit x))

The total log weight of a biased coordinate is bounded using only its rare count.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.sum_log_messageWeight_ge {X : Type u_1} {ι : Type u_2} [Fintype X] [Fintype ι] (key : X → ι → Bool) (biased : Finset ι) (rare : ι → Bool) (bias : ∀ i ∈ biased, 4 * {x : X | key x i = rare i}.card ≤ Fintype.card X) : -↑(Fintype.card X) * (↑(Fintype.card ι) * Real.log 2 - ↑biased.card * biasSaving) ≤ ∑ x : X, Real.log (messageWeight (fun (i : ι) => decide (i ∈ biased)) rare (key x))

A product log weight charges every biased coordinate without assuming independence.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.log_card_le_of_fibres_and_bias {X : Type u_1} {ι : Type u_2} [Fintype X] [Nonempty X] [Fintype ι] (key : X → ι → Bool) (biased : Finset ι) (rare : ι → Bool) {K : ℕ} (hK : 0 < K) (fibres : ∀ (message : ι → Bool), {x : X | key x = message}.card ≤ K) (bias : ∀ i ∈ biased, 4 * {x : X | key x i = rare i}.card ≤ Fintype.card X) : Real.log ↑(Fintype.card X) ≤ Real.log ↑K + ↑(Fintype.card ι) * Real.log 2 - ↑biased.card * biasSaving

A product distribution yields the exact entropy saving without independence assumptions.