Bloom filter

StructureBloom filter#✓fully proved

A Bloom filter over a type \(\alpha\) with \(m\) bits consists of a finite list of hash functions \(\alpha \to \{0, \dots, m - 1\}\) and a bit vector of length \(m\).

No false-positive rate is claimed because the model supplies no probability distribution.

public structure BloomFilter (α : Type u) (m : Nat) where
  /-- The hash functions; bit `h x` is set when `x` is inserted, for each `h` in the list. -/
  hashes : List (α → Fin m)
  /-- The bit vector. Bits start unset and are only ever set. -/
  bits : Vector Bool m

Used by 12

Used byBits set after inserting a list into a Bloom filter · Bits set by an insertion · Empty Bloom filter · Bloom filter insertion keeps the hash functions · Bloom filter insertion · Inserting a list of elements into a Bloom filter · Bloom filter membership query · The empty Bloom filter reports every element absent · Membership query in terms of bits · Characterization of the Bloom filter false-positive event · Insertion preserves positive answers · An inserted element is reported present

DefinitionEmpty Bloom filter#✓fully proved

Let \(\alpha\) be a type and \(m\) a natural number. Given a list of hash functions \(\alpha \to \{0, \dots, m - 1\}\), the empty Bloom filter with these hash functions has all of its \(m\) bits unset.

public def empty {α : Type u} {m : Nat} (hashes : List (α → Fin m)) : BloomFilter α m where
  hashes := hashes
  bits := Vector.replicate m false

Uses 1 · Used by 2

Statement usesBloom filter

Used byThe empty Bloom filter reports every element absent · Characterization of the Bloom filter false-positive event

DefinitionBloom filter insertion#✓fully proved

Inserting an element \(x\) into a Bloom filter keeps its hash functions and sets bit \(h(x)\) for every hash function \(h\) of the filter, leaving all other bits unchanged.

public def insert {α : Type u} {m : Nat} (filter : BloomFilter α m) (x : α) :
    BloomFilter α m where
  hashes := filter.hashes
  bits := filter.hashes.foldl (fun bits h => bits.set (h x) true) filter.bits

Uses 1 · Used by 6

Statement usesBloom filter

Used byBits set after inserting a list into a Bloom filter · Bits set by an insertion · Bloom filter insertion keeps the hash functions · Inserting a list of elements into a Bloom filter · Insertion preserves positive answers · An inserted element is reported present

DefinitionBloom filter membership query#✓fully proved

A Bloom filter reports that an element \(x\) may be present when bit \(h(x)\) is set for every hash function \(h\) of the filter, and reports \(x\) absent otherwise.

public def mayContain {α : Type u} {m : Nat} (filter : BloomFilter α m) (x : α) : Bool :=
  filter.hashes.all fun h => filter.bits[h x]

Uses 1 · Used by 5

Statement usesBloom filter

Used byThe empty Bloom filter reports every element absent · Membership query in terms of bits · Characterization of the Bloom filter false-positive event · Insertion preserves positive answers · An inserted element is reported present

TheoremBits set by an insertion#✓fully proved

Let \(F\) be a Bloom filter over \(\alpha\) with \(m\) bits, let \(x \in \alpha\) and let \(i \in \{0, \dots, m - 1\}\). Bit \(i\) of the filter obtained by inserting \(x\) into \(F\) is set if and only if bit \(i\) of \(F\) is set or some hash function \(h\) of \(F\) satisfies \(h(x) = i\).

public theorem bit_insert_iff {α : Type u} {m : Nat} (filter : BloomFilter α m)
    (x : α) (i : Fin m) :
    (filter.insert x).bits[i] = true ↔
      filter.bits[i] = true ∨ ∃ h ∈ filter.hashes, h x = i

Uses 2 · Used by 3

Statement usesBloom filter · Bloom filter insertion

Used byBits set after inserting a list into a Bloom filter · Insertion preserves positive answers · An inserted element is reported present

TheoremMembership query in terms of bits#✓fully proved

For a Bloom filter \(F\) and an element \(x\), \(F\) reports that \(x\) may be present if and only if bit \(h(x)\) of \(F\) is set for every hash function \(h\) of \(F\).

public theorem mayContain_iff {α : Type u} {m : Nat} (filter : BloomFilter α m) (x : α) :
    filter.mayContain x = true ↔ ∀ h ∈ filter.hashes, filter.bits[h x] = true

Uses 2 · Used by 3

Statement usesBloom filter · Bloom filter membership query

Used byCharacterization of the Bloom filter false-positive event · Insertion preserves positive answers · An inserted element is reported present

TheoremAn inserted element is reported present#✓fully proved

For every Bloom filter \(F\) and element \(x\), the filter obtained by inserting \(x\) into \(F\) reports that \(x\) may be present.

public theorem mayContain_insert_self {α : Type u} {m : Nat} (filter : BloomFilter α m)
    (x : α) : (filter.insert x).mayContain x = true

Uses 5

Statement usesBloom filter · Bloom filter insertion · Bloom filter membership query

Proof usesBits set by an insertion · Membership query in terms of bits

TheoremInsertion preserves positive answers#✓fully proved

Let \(F\) be a Bloom filter and let \(x\), \(y\) be elements. If \(F\) reports that \(x\) may be present, then so does the filter obtained by inserting \(y\) into \(F\).

Insertion never clears a bit, so an element reported present stays reported present after any later insertion; in particular there are no false negatives under further inserts.

public theorem mayContain_insert_mono {α : Type u} {m : Nat} (filter : BloomFilter α m)
    (x y : α) (present : filter.mayContain x = true) :
    (filter.insert y).mayContain x = true

Uses 5

Statement usesBloom filter · Bloom filter insertion · Bloom filter membership query

Proof usesBits set by an insertion · Membership query in terms of bits

TheoremThe empty Bloom filter reports every element absent#✓fully proved

Let \(\alpha\) be a type, \(m\) a natural number and \(H\) a nonempty list of hash functions \(\alpha \to \{0, \dots, m - 1\}\). For every element \(x \in \alpha\), the empty Bloom filter with hash functions \(H\) reports \(x\) absent.

public theorem mayContain_empty {α : Type u} {m : Nat} {hashes : List (α → Fin m)}
    (nonempty : hashes ≠ []) (x : α) :
    (empty hashes).mayContain x = false

Uses 3

Statement usesEmpty Bloom filter · Bloom filter membership query

Proof usesBloom filter

DefinitionInserting a list of elements into a Bloom filter#✓fully proved

Insert every element of a list, left to right.

def insertAll (filter : BloomFilter α m) (xs : List α) : BloomFilter α m :=
  xs.foldl BloomFilter.insert filter

Uses 2 · Used by 3

Statement usesBloom filter · Bloom filter insertion

Used byBits set after inserting a list into a Bloom filter · Bloom filter insertion keeps the hash functions · Characterization of the Bloom filter false-positive event

TheoremBloom filter insertion keeps the hash functions#✓fully proved

Insertion keeps the hash functions.

theorem hashes_insertAll (filter : BloomFilter α m) (xs : List α) :
    (filter.insertAll xs).hashes = filter.hashes

Uses 3 · Used by 1

Statement usesBloom filter · Inserting a list of elements into a Bloom filter

Proof usesBloom filter insertion

Used byCharacterization of the Bloom filter false-positive event

TheoremBits set after inserting a list into a Bloom filter#✓fully proved

After inserting a list, bit i is set iff it was set before or some hash function sends some inserted element to i.

theorem bit_insertAll_iff (filter : BloomFilter α m) (xs : List α) (i : Fin m) :
    (filter.insertAll xs).bits[i] = true ↔
      filter.bits[i] = true ∨ ∃ x ∈ xs, ∃ h ∈ filter.hashes, h x = i

Uses 4 · Used by 1

Statement usesBloom filter · Inserting a list of elements into a Bloom filter

Proof usesBits set by an insertion · Bloom filter insertion

Used byCharacterization of the Bloom filter false-positive event

TheoremCharacterization of the Bloom filter false-positive event#✓fully proved

The false-positive event: after inserting xs into an empty filter, y is reported present iff every bit selected by y is selected by some stored element.

theorem mayContain_insertAll_empty_iff (hashes : List (α → Fin m)) (xs : List α) (y : α) :
    ((empty hashes).insertAll xs).mayContain y = true ↔
      ∀ h ∈ hashes, ∃ x ∈ xs, ∃ h' ∈ hashes, h' x = h y

Uses 7

Statement usesEmpty Bloom filter · Inserting a list of elements into a Bloom filter · Bloom filter membership query

Proof usesBloom filter · Bits set after inserting a list into a Bloom filter · Bloom filter insertion keeps the hash functions · Membership query in terms of bits

DefinitionBits set by the stored hash values#✓fully proved

The bits set by the stored hash values H a j (element a, hash function j).

def setBits (H : Fin n → Fin k → Fin m) : Finset (Fin m) :=
  univ.image fun p : Fin n × Fin k => H p.1 p.2

Used by 7

Used byNumber of hash outcomes leaving a given bit unset · Bloom's formula is a lower bound · Expected fraction of set bits in a Bloom filter · Exact Bloom filter false-positive rate under uniform hashing · False-positive rate as the expected k-th power of the set fraction · A Bloom filter bit is unset iff no stored hash selects it · Probability that a given Bloom filter bit is unset

TheoremA Bloom filter bit is unset iff no stored hash selects it#✓fully proved

A bit is unset iff no stored hash value selects it.

theorem notMem_setBits_iff (H : Fin n → Fin k → Fin m) (i : Fin m) :
    i ∉ setBits H ↔ ∀ a j, H a j ≠ i

Uses 1 · Used by 1

Statement usesBits set by the stored hash values

Used byNumber of hash outcomes leaving a given bit unset

DefinitionExact Bloom filter false-positive rate under uniform hashing#✓fully proved

The exact false-positive rate under uniform hashing: the fraction of outcomes (stored hash values H, query hash values q) in which every query bit is set.

noncomputable def falsePositiveProb : ℝ :=
  (#{Hq : (Fin n → Fin k → Fin m) × (Fin k → Fin m) | ∀ j, Hq.2 j ∈ setBits Hq.1} : ℝ) /
    Fintype.card ((Fin n → Fin k → Fin m) × (Fin k → Fin m))

Uses 1 · Used by 3

Statement usesBits set by the stored hash values

Used byBloom's formula is a lower bound · Exponential approximation is a lower bound on the false-positive rate · False-positive rate as the expected k-th power of the set fraction

TheoremNumber of hash outcomes leaving a given bit unset#✓fully proved

Exactly (m - 1) ^ (n * k) outcomes of the stored hash values leave bit i unset.

theorem card_unset (i : Fin m) :
    #{H : Fin n → Fin k → Fin m | i ∉ setBits H} = (m - 1) ^ (n * k)

Uses 2 · Used by 2

Statement usesBits set by the stored hash values

Proof usesA Bloom filter bit is unset iff no stored hash selects it

Used byExpected fraction of set bits in a Bloom filter · Probability that a given Bloom filter bit is unset

TheoremProbability that a given Bloom filter bit is unset#✓fully proved

A given bit is unset with probability (1 - 1/m) ^ (n * k).

theorem prob_unset (hm : 0 < m) (i : Fin m) :
    (#{H : Fin n → Fin k → Fin m | i ∉ setBits H} : ℝ) /
      Fintype.card (Fin n → Fin k → Fin m) = (1 - 1 / (m : ℝ)) ^ (n * k)

Uses 2

Statement usesBits set by the stored hash values

Proof usesNumber of hash outcomes leaving a given bit unset

TheoremExpected fraction of set bits in a Bloom filter#✓fully proved

The expected fraction of set bits is 1 - (1 - 1/m) ^ (n * k).

theorem expected_fraction_set (hm : 0 < m) :
    (∑ H : Fin n → Fin k → Fin m, (#(setBits H) : ℝ) / m) /
      Fintype.card (Fin n → Fin k → Fin m) = 1 - (1 - 1 / (m : ℝ)) ^ (n * k)

Uses 2 · Used by 1

Statement usesBits set by the stored hash values

Proof usesNumber of hash outcomes leaving a given bit unset

Used byBloom's formula is a lower bound

TheoremFalse-positive rate as the expected k-th power of the set fraction#✓fully proved

The exact false-positive rate is the expectation of (fraction of set bits) ^ k.

theorem falsePositiveProb_eq (hm : 0 < m) :
    falsePositiveProb m n k =
      (∑ H : Fin n → Fin k → Fin m, ((#(setBits H) : ℝ) / m) ^ k) /
        Fintype.card (Fin n → Fin k → Fin m)

Uses 2 · Used by 1

Statement usesExact Bloom filter false-positive rate under uniform hashing · Bits set by the stored hash values

Used byBloom's formula is a lower bound

TheoremBloom's formula is a lower bound#✓fully proved

Bloom's formula is a lower bound on the exact false-positive rate (Jensen's inequality for t ↦ t ^ k).

theorem classical_le_falsePositiveProb (hm : 0 < m) :
    (1 - (1 - 1 / (m : ℝ)) ^ (n * k)) ^ k ≤ falsePositiveProb m n k

Uses 4 · Used by 1

Statement usesExact Bloom filter false-positive rate under uniform hashing

Proof usesExpected fraction of set bits in a Bloom filter · False-positive rate as the expected k-th power of the set fraction · Bits set by the stored hash values

Used byExponential approximation is a lower bound on the false-positive rate

TheoremExponential approximation is a lower bound on the false-positive rate#✓fully proved

The exponential approximation (1 - exp (-(k n) / m)) ^ k is also a lower bound.

theorem exp_approx_le_falsePositiveProb (hm : 0 < m) :
    (1 - Real.exp (-((n * k : ℕ) : ℝ) / m)) ^ k ≤ falsePositiveProb m n k

Uses 2

Statement usesExact Bloom filter false-positive rate under uniform hashing

Proof usesBloom's formula is a lower bound

TheoremBound \(\log t \cdot \log(1-t) \le (\log 2)^2\) on the unit interval#✓fully proved

log t * log (1 - t) ≤ (log 2) ^ 2 on (0, 1).

theorem log_mul_log_one_sub_le {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) :
    Real.log t * Real.log (1 - t) ≤ Real.log 2 ^ 2

Used by 1

Used byThe optimal number of hash functions

TheoremEquality in the log-product bound holds only at \(t = 1/2\)#✓fully proved

Equality holds only at t = 1 / 2.

theorem log_mul_log_one_sub_eq_iff {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) :
    Real.log t * Real.log (1 - t) = Real.log 2 ^ 2 ↔ t = 1 / 2

DefinitionExponential approximation of the Bloom filter false-positive rate#✓fully proved

The exponential approximation (1 - exp (-κ n / m)) ^ κ of the false-positive rate, as a function of a real number κ of hash functions.

noncomputable def expApprox (m n : ℕ) (κ : ℝ) : ℝ := (1 - Real.exp (-κ * n / m)) ^ κ

Used by 2

Used byExponential approximation at the optimal number of hash functions · The optimal number of hash functions

TheoremExponential approximation at the optimal number of hash functions#✓fully proved

At κ = (m / n) log 2 half of the bits are expected to be set and the approximation is (1 / 2) ^ κ.

theorem expApprox_at_optimum {m n : ℕ} (hm : 0 < m) (hn : 0 < n) :
    expApprox m n (m / n * Real.log 2) = (1 / 2) ^ ((m : ℝ) / n * Real.log 2)

Uses 1 · Used by 1

Statement usesExponential approximation of the Bloom filter false-positive rate

Used byThe optimal number of hash functions

TheoremThe optimal number of hash functions#✓fully proved

The optimal number of hash functions for the exponential approximation: on real κ > 0, (1 - exp (-κ n / m)) ^ κ is minimal at κ = (m / n) log 2.

theorem expApprox_optimal {m n : ℕ} (hm : 0 < m) (hn : 0 < n) {κ : ℝ} (hκ : 0 < κ) :
    expApprox m n (m / n * Real.log 2) ≤ expApprox m n κ

Uses 3

Statement usesExponential approximation of the Bloom filter false-positive rate

Proof usesExponential approximation at the optimal number of hash functions · Bound \(\log t \cdot \log(1-t) \le (\log 2)^2\) on the unit interval

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.