OAI/NumberTheory/Ostmann/Construction/CollisionTestTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.residueTestError line 12
2. theorem OAI.Ostmann.residueTestError_eq line 15
3. theorem OAI.Ostmann.residueTestError_sq_le line 21
4. theorem OAI.Ostmann.collisionDefect_controls_tests line 38
5. theorem OAI.Ostmann.weighted_collision_test_errors line 55

   Source documentation

   The complete weighted collision budget bounds the empirical test errors, even when each test is chosen independently at its prime.

   theorem weighted_collision_test_errors (P : Finset ℕ) (S T : ℕ → Finset ℕ)
       (μ ν f g : ℕ → ℕ → ℝ) (hP : ∀ p ∈ P, p.Prime)
       (hS : ∀ p ∈ P, (S p).Nonempty) (hT : ∀ p ∈ P, (T p).Nonempty)
       (hcard : ∀ p ∈ P, (S p).card + (T p).card ≤ p)
       (hf : ∀ p ∈ P, ∀ r ∈ S p, |f p r| ≤ 1)
       (hg : ∀ p ∈ P, ∀ r ∈ T p, |g p r| ≤ 1) :
       (∑ p ∈ P, (Real.log (p : ℝ) / p) *
         (residueTestError (S p) (μ p) (f p) ^ 2 + residueTestError (T p) (ν p) (g p) ^ 2)) ≤
       ∑ p ∈ P, Real.log (p : ℝ) * collisionDefect p (S p) (T p) (μ p) (ν p) := by
   …

   Mentions: OAI.Ostmann.residueTestError, OAI.Ostmann.collisionDefect