Fiber counts and collisions of a finite hash family #

All identities count source-seed pairs with multiplicity. Squaring the fiber counts counts colliding source pairs, including the diagonal.

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

The number of source points with a given seed-output pair, as a real number.

Equations

Instances For

theorem Algebraic.Cutwidth.Extractor.Internal.hashFiberCount_sum_output {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Ω] (E : α → Seed → Ω) (y : Seed) :

theorem Algebraic.Cutwidth.Extractor.Internal.hashFiberCount_sum {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] (E : α → Seed → Ω) :

∑ z : Seed × Ω, hashFiberCount E z = ↑(Fintype.card Seed) * ↑(Fintype.card α)

theorem Algebraic.Cutwidth.Extractor.Internal.hashFiberCount_sq_sum_output {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Ω] (E : α → Seed → Ω) (y : Seed) :

∑ o : Ω, hashFiberCount E (y, o) ^ 2 = ∑ x : α, ∑ x' : α, if E x y = E x' y then 1 else 0

theorem Algebraic.Cutwidth.Extractor.Internal.hashFiberCount_sq_sum {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] (E : α → Seed → Ω) :

∑ z : Seed × Ω, hashFiberCount E z ^ 2 = ∑ x : α, ∑ x' : α, ↑{y : Seed | E x y = E x' y}.card

theorem Algebraic.Cutwidth.Extractor.Internal.hashFiberCount_sum_test {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] (E : α → Seed → Ω) (T : Finset (Seed × Ω)) :

∑ z ∈ T, hashFiberCount E z = ↑{xy : α × Seed | (xy.2, E xy.1 xy.2) ∈ T}.card

theorem Algebraic.Cutwidth.Extractor.Internal.seededTestProb_eq_hashFiberCount {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] (E : α → Seed → Ω) (T : Finset (Seed × Ω)) :

Documentation