HarmonicTestTransfer.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Harmonic test errors from the full collision budget

theorem OAI.Ostmann.uniform_fiber_test_error line 11

theorem OAI.Ostmann.harmonic_collision_test_errors line 21

Source documentation

Passing from the log(p) collision budget to harmonic mass only loses the reciprocal of the smallest log(p) in the tested set.

theorem harmonic_collision_test_errors (P R : Finset ℕ) (hPR : P ⊆ R)
    (S T : ℕ → Finset ℕ) (μ ν f : ℕ → ℕ → ℝ) (B E : ℝ) (hB : 0 < B)
    (hprime : ∀ p ∈ R, p.Prime)
    (hS : ∀ p ∈ R, (S p).Nonempty) (hT : ∀ p ∈ R, (T p).Nonempty)
    (hcard : ∀ p ∈ R, (S p).card + (T p).card ≤ p)
    (hf : ∀ p ∈ P, ∀ r ∈ S p, |f p r| ≤ 1)
    (hlog : ∀ p ∈ P, B ≤ Real.log (p : ℝ))
    (hbudget : (∑ p ∈ R, Real.log (p : ℝ) *
      collisionDefect p (S p) (T p) (μ p) (ν p)) ≤ E) :
    (∑ p ∈ P, (p : ℝ)⁻¹ * residueTestError (S p) (μ p) (f p) ^ 2) ≤ E / B := by
…

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