One-way bounds from joint message weights #
Any normalized joint weight certificate can replace the separate-coordinate product distribution in the rectangle-free message bound.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Joint.sender_card_le_of_weight_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)
{Y : Type u_1}
[Fintype Y]
(summary : OneWaySummary f U Y)
{cost : ℝ}
(certificate : Entropy.WeightBound summary.key cost)
:
A joint message cost bounds the number of sending-side input bits.