SplitCollision.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The final split-prime collision contradiction

Finite quantitative form of the last step in Proposition 3.1. The inputs about which primes split and the root populations are intermediate claims of that proposition, not published inputs and not asserted here.

theorem OAI.Ostmann.split_collision_lower_bound line 19

Source documentation

Split primes double the universal lower bound for the combined collision probability of the two root populations.

theorem split_collision_lower_bound (P R : Finset ℕ) (β₁ β₂ : ℕ → ℝ)
    (hRP : R ⊆ P) (hP : ∀ p ∈ P, p.Prime)
    (hbase : ∀ p ∈ P, 2 / (p : ℝ) ≤ β₁ p + β₂ p)
    (hsplit : ∀ p ∈ R, 4 / (p : ℝ) ≤ β₁ p + β₂ p) :
    2 * (∑ p ∈ P, Real.log (p : ℝ) / (p : ℝ)) +
      2 * (∑ p ∈ R, Real.log (p : ℝ) / (p : ℝ)) ≤
      ∑ p ∈ P, Real.log (p : ℝ) * (β₁ p + β₂ p) := by
…

theorem OAI.Ostmann.split_collision_scale_bound line 67

Source documentation

Explicit constants for the collision contradiction in Proposition 3.1. Once the asymptotic errors are at most L/100, the log scale is bounded by 50 C; hence these hypotheses cannot persist on unbounded scales.

theorem split_collision_scale_bound (P R : Finset ℕ) (β₁ β₂ : ℕ → ℝ)
    (L η C : ℝ) (hRP : R ⊆ P) (hP : ∀ p ∈ P, p.Prime)
    (hbase : ∀ p ∈ P, 2 / (p : ℝ) ≤ β₁ p + β₂ p)
    (hsplit : ∀ p ∈ R, 4 / (p : ℝ) ≤ β₁ p + β₂ p)
    (hL : 0 ≤ L) (hη : η ≤ 1 / 1000)
    (hmertens : (1 / 2 - 5 * η) * L - C ≤
      ∑ p ∈ P, Real.log (p : ℝ) / (p : ℝ))
    (hsplitmass : (3 / 100) * L ≤ ∑ p ∈ R, Real.log (p : ℝ) / (p : ℝ))
    (hupper : (∑ p ∈ P, Real.log (p : ℝ) * (β₁ p + β₂ p)) ≤ (101 / 100) * L) :
    L ≤ 50 * C := by
…