Collision control of the centered second moment

Universal hashing controls off-diagonal collisions. The diagonal contributes one inverse source-cardinality term. A test on a zero-sum vector is half of its pairing with a sign vector, giving the sharp factor of one quarter after Cauchy--Schwarz and squaring.

noncomputable def Algebraic.Cutwidth.Extractor.Internal.hashCenteredCount {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Ω] (E : α → Seed → Ω) (z : Seed × Ω) : ℝ

Fiber counts centered and scaled to avoid division in the counting proof.

Equations

• Algebraic.Cutwidth.Extractor.Internal.hashCenteredCount E z = ↑(Fintype.card Ω) * Algebraic.Cutwidth.Extractor.Internal.hashFiberCount E z - ↑(Fintype.card α)

theorem Algebraic.Cutwidth.Extractor.Internal.universalHash_collision_sum_le {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] {E : α → Seed → Ω} (universal : UniversalHashFamily E) : ↑(Fintype.card Ω) * ∑ z : Seed × Ω, hashFiberCount E z ^ 2 ≤ ↑(Fintype.card Seed) * ↑(Fintype.card α) ^ 2 + ↑(Fintype.card α) * ↑(Fintype.card Seed) * ↑(Fintype.card Ω)

theorem Algebraic.Cutwidth.Extractor.Internal.hashCenteredCount_sum {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] (E : α → Seed → Ω) : ∑ z : Seed × Ω, hashCenteredCount E z = 0

theorem Algebraic.Cutwidth.Extractor.Internal.hashCenteredCount_sq_sum_le {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] {E : α → Seed → Ω} (universal : UniversalHashFamily E) : ∑ z : Seed × Ω, hashCenteredCount E z ^ 2 ≤ ↑(Fintype.card Seed) * ↑(Fintype.card Ω) ^ 2 * ↑(Fintype.card α)

theorem Algebraic.Cutwidth.Extractor.Internal.zero_sum_test_sq_le {ι : Type u_1} [Fintype ι] (a : ι → ℝ) (mass : ∑ i : ι, a i = 0) (T : Finset ι) : 4 * (∑ i ∈ T, a i) ^ 2 ≤ ↑(Fintype.card ι) * ∑ i : ι, a i ^ 2