MinHash and Jaccard similarity

DefinitionMin-hash of a set under a permutation#✓fully proved

The min-hash of A under the permutation π: the least element of π(A), or ⊤ if A is empty.

def minHash (π : Equiv.Perm U) (A : Finset U) : WithTop U := (A.image π).min

Used by 2

Used byMinHash, counting form · MinHash collision probability

TheoremMinHash, counting form#✓fully proved

The number of permutations of U under which A and B have the same min-hash, times |A ∪ B|, equals |A ∩ B| times the number of all permutations.

theorem card_minHash_collision [Fintype U] (A B : Finset U) (hC : (A ∪ B).Nonempty) :
    (univ.filter fun π : Equiv.Perm U => minHash π A = minHash π B).card * (A ∪ B).card =
      (A ∩ B).card * Fintype.card (Equiv.Perm U)

Uses 1 · Used by 1

Statement usesMin-hash of a set under a permutation

Used byMinHash collision probability

TheoremMinHash collision probability#✓fully proved

MinHash collision probability (Broder 1997): for a uniformly random permutation π of the finite universe U (uniformOn Set.univ on Equiv.Perm U, for any measurable structure in which singletons are measurable, e.g. ⊤) and sets A, B with A ∪ B nonempty, P(min π(A) = min π(B)) = |A ∩ B| / |A ∪ B|, the Jaccard similarity of A and B.

theorem uniformOn_minHash_collision [Finite U] [MeasurableSpace (Equiv.Perm U)]
    [MeasurableSingletonClass (Equiv.Perm U)] (A B : Finset U) (hC : (A ∪ B).Nonempty) :
    ProbabilityTheory.uniformOn Set.univ {π : Equiv.Perm U | minHash π A = minHash π B} =
      ((A ∩ B).card : ENNReal) / (A ∪ B).card

Uses 2

Statement usesMin-hash of a set under a permutation

Proof usesMinHash, counting form

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.