@[reducible, inline]

abbrev CommunicationComplexity.Functions.Hash.HashSpace (α : Type u_1) (k : ℕ) : Type u_1

A hash function on α with outputs in Fin k.

Equations

• CommunicationComplexity.Functions.Hash.HashSpace α k = (α → Fin k)

noncomputable instance CommunicationComplexity.Functions.Hash.hashRange.measureSpace (k : ℕ) : MeasureTheory.MeasureSpace (Fin k)

Equations

• CommunicationComplexity.Functions.Hash.hashRange.measureSpace k = { toMeasurableSpace := Fin.instMeasurableSpace k, volume := ProbabilityTheory.uniformOn Set.univ }

instance CommunicationComplexity.Functions.Hash.hashRange.isProbabilityMeasure (k : ℕ) [NeZero k] : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable instance CommunicationComplexity.Functions.Hash.hashRange.finiteProbabilitySpace (k : ℕ) [NeZero k] : FiniteProbabilitySpace (Fin k)

Equations

• CommunicationComplexity.Functions.Hash.hashRange.finiteProbabilitySpace k = CommunicationComplexity.FiniteProbabilitySpace.of (Fin k)

noncomputable instance CommunicationComplexity.Functions.Hash.hashSpace.finiteProbabilitySpace (α : Type u_1) [Fintype α] (k : ℕ) [NeZero k] : FiniteProbabilitySpace (HashSpace α k)

Equations

• CommunicationComplexity.Functions.Hash.hashSpace.finiteProbabilitySpace α k = inferInstance

theorem CommunicationComplexity.Functions.Hash.collision_prob_le (α : Type u_1) [Fintype α] (k : ℕ) [NeZero k] (x y : α) (hxy : x ≠ y) : MeasureTheory.volume.real {h : HashSpace α k | h x = h y} ≤ 1 / ↑k

For distinct inputs, a uniformly random hash collides with probability 1 / k.