A one-way bit bound with biased coordinates

The two-sided rectangle obstruction bounds message fibres. Product-weight counting then subtracts the exact binary-entropy deficit of every quarter-biased message bit.

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

The saving in bits from a coordinate with rare probability at most one quarter.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitSaving = Algebraic.Cutwidth.Aggregate.Geometry.Entropy.biasSaving / Real.log 2

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitSaving_pos : 0 < bitSaving

A quarter-biased bit saves a strictly positive amount of information.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.bitSaving_eq : bitSaving = 1 - Real.binEntropy (1 / 4) / Real.log 2

The saving is one minus the binary entropy in base two.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.input_le_bits_of_biased_oneWay {n K : ℕ} {f : Cslib.BooleanFunction n} (hK : 0 < K) (free : RectangleFree f K) (freeNot : RectangleFree (fun (x : Cslib.BitString n) => !f x) K) (U : Finset (Fin n)) (large : 2 * K ≤ 2 ^ Uᶜ.card) {ι : Type u_1} [Fintype ι] (summary : OneWaySummary f U (ι → Bool)) (biased : Finset ι) (rare : ι → Bool) (bias : ∀ i ∈ biased, 4 * {x : ↥U → Bool | summary.key x i = rare i}.card ≤ 2 ^ U.card) : ↑n ≤ ↑(Fintype.card ι) + ↑Uᶜ.card + Real.logb 2 ↑K - ↑biased.card * bitSaving

Exact one-way communication bound, including a saving for each biased bit.