Collision.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Elementary collision estimates

These are the finite probability and support-size inequalities used in §2 and in the final collision argument of §3. No analytic estimate is assumed.

theorem OAI.Ostmann.inverse_card_le_collision line 24
Source documentation
Cauchy--Schwarz bounds the collision probability of a unit mass on a finite nonempty support by the reciprocal of the support's size.
```
theorem inverse_card_le_collision {α : Type*} (s : Finset α) (μ : α → ℝ)
    (hs : s.Nonempty) (hmass : ∑ x ∈ s, μ x = 1) :
    1 / (s.card : ℝ) ≤ ∑ x ∈ s, μ x ^ 2 := by
…
```

theorem OAI.Ostmann.collision_sub_uniform line 34

Source documentation

Exact squared distance from uniform probability on a finite support.

theorem collision_sub_uniform {α : Type*} (s : Finset α) (μ : α → ℝ)
    (hs : s.Nonempty) (hmass : ∑ x ∈ s, μ x = 1) :
    ∑ x ∈ s, (μ x - 1 / (s.card : ℝ)) ^ 2 =
      (∑ x ∈ s, μ x ^ 2) - 1 / (s.card : ℝ) := by
…

theorem OAI.Ostmann.four_div_le_inverse_add_inverse line 56
Source documentation
Disjoint nonempty supports occupying at most p residues have combined collision probability at least 4 / p.
```
theorem four_div_le_inverse_add_inverse {a b p : ℝ}
    (ha : 0 < a) (hb : 0 < b) (hab : a + b ≤ p) :
    4 / p ≤ 1 / a + 1 / b := by
…
```

theorem OAI.Ostmann.collision_lower_bound_disjoint line 71

Source documentation

The combined collision lower bound on disjoint residue supports, as used at the split primes in the last paragraph of §3.

theorem collision_lower_bound_disjoint {α : Type*} [Fintype α]
    (s t : Finset α) (μ ν : α → ℝ)
    (hs : s.Nonempty) (ht : t.Nonempty) (hst : Disjoint s t)
    (hμ : ∑ x ∈ s, μ x = 1) (hν : ∑ x ∈ t, ν x = 1) :
    4 / (Fintype.card α : ℝ) ≤
      (∑ x ∈ s, μ x ^ 2) + ∑ x ∈ t, ν x ^ 2 := by
…