Collision budgets for biased Boolean features

An average collision bound replaces the maximum-fibre hypothesis in weighted counting. Dividing each pulled-back message weight by its fibre size normalizes the mass; two logarithmic mean inequalities then charge biased coordinates. No independence assumption is made on the features.

The differential-uniformity collision estimate used by applications is classical: Kölsch, Kriepke, and Kyureghyan, "Image sets of perfectly nonlinear maps" (2022), Lemma 2 and Corollary 1, https://doi.org/10.1007/s10623-022-01094-4.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.collisionCount {X : Type u_1} {T : Type u_2} [Fintype X] (key : X → T) : ℕ

The number of ordered pairs of inputs with equal keys, including the diagonal.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.collisionCount key = ∑ x : X, {y : X | key y = key x}.card

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.collisionCount_le_of_refines {X : Type u_1} {T : Type u_2} {U : Type u_3} [Fintype X] (key : X → T) (coarse : X → U) (refines : ∀ (x y : X), key x = key y → coarse x = coarse y) : collisionCount key ≤ collisionCount coarse

Refining equality of keys cannot increase their number of collisions.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.collisionCount_eq_sum_differences {X : Type u_1} {T : Type u_2} [Fintype X] [AddGroup X] (key : X → T) : collisionCount key = ∑ d : X, {x : X | key (x + d) = key x}.card

Reindex ordered collisions by their input displacement.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.collisionCount_le_of_differences {X : Type u_1} {T : Type u_2} [Fintype X] [AddGroup X] (key : X → T) {δ : ℕ} (differences : ∀ (d : X), d ≠ 0 → {x : X | key (x + d) = key x}.card ≤ δ) : collisionCount key ≤ Fintype.card X + δ * (Fintype.card X - 1)

A bound on every nonzero difference gives the classical ordered-collision budget.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.sum_weight_div_fibre_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) : ∑ x : X, weight (key x) / ↑{y : X | key y = key x}.card ≤ 1

Dividing pulled-back weights by their fibre sizes leaves mass at most one.

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

Average collisions, rather than the largest fibre, suffice to charge biased features.