RootCollisions.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Collisions of uniform root populations

The root populations at the end of §3 occupy translated intervals. Their collision upper bound depends on the diameter and their cardinality.

theorem OAI.Ostmann.sum_uniform_mass line 18
def OAI.Ostmann.uniformResidueCollision line 25
Source documentation
Probability that two uniform elements of s are congruent modulo p.
```
noncomputable def uniformResidueCollision (s : Finset ℕ) (p : ℕ) : ℝ :=
…
```
theorem OAI.Ostmann.uniformResidueCollision_lower line 28
theorem OAI.Ostmann.uniformResidueCollision_upper line 37

theorem OAI.Ostmann.uniformResidueCollision_lower_of_disjoint_images line 48

Source documentation

Disjoint residue images, after an injective relabeling on each side, force the stronger lower bound at a split prime.

theorem uniformResidueCollision_lower_of_disjoint_images (s t : Finset ℕ)
    (hs : s.Nonempty) (ht : t.Nonempty) {p : ℕ} (hp : 0 < p)
    (f g : ℕ → ℕ)
    (hf : ∀ a ∈ s, f a < p) (hg : ∀ b ∈ t, g b < p)
    (hfc : ∀ a ∈ s, ∀ b ∈ s, f a = f b ↔ a ≡ b [MOD p])
    (hgc : ∀ a ∈ t, ∀ b ∈ t, g a = g b ↔ a ≡ b [MOD p])
    (hdisjoint : Disjoint (s.image f) (t.image g)) :
    4 / (p : ℝ) ≤ uniformResidueCollision s p + uniformResidueCollision t p := by
…

Mentions: OAI.Ostmann.uniformResidueCollision

theorem OAI.Ostmann.uniformResidueCollision_lower_of_scaled_disjoint line 95

Source documentation

Multiplying one population by a nonzero field element preserves its collision probability. Thus disjoint scaled root residues give 4 / p.

theorem uniformResidueCollision_lower_of_scaled_disjoint {p : ℕ} [Fact p.Prime]
    (s t : Finset ℕ) (hs : s.Nonempty) (ht : t.Nonempty) (c : ZMod p) (hc : c ≠ 0)
    (hdisjoint : Disjoint (s.image (fun a : ℕ => (a : ZMod p)))
      (t.image (fun b : ℕ => c * (b : ZMod p)))) :
    4 / (p : ℝ) ≤ uniformResidueCollision s p + uniformResidueCollision t p := by
…

Mentions: OAI.Ostmann.uniformResidueCollision