SplitMassNumerics.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit numerical margin in the split-prime estimate

theorem OAI.Ostmann.exp_neg_twelve_fifths_le line 12
theorem OAI.Ostmann.split_prime_tail_factor_bound line 22
Source documentation
A cutoff whose logarithm is at least 0.48L suffices for the exponent comparison tail. The later choices have logarithm asymptotic to 0.5L.
```
theorem split_prime_tail_factor_bound (Q : ℕ) (L : ℝ) (hQ : 0 < Q) (hL : 0 < L)
    (hlog : (12 / 25 : ℝ) * L ≤ Real.log (Q : ℝ)) :
    (Q : ℝ) ^ (-(10 / L) / 2) ≤ 1 / 11 := by
…
```

theorem OAI.Ostmann.split_mass_numeric_margin line 38

Source documentation

The elementary margin leaves room for all constant and Siegel errors.

theorem split_mass_numeric_margin (L C B E t : ℝ) (hL : 0 ≤ L) (hC : 0 ≤ C)
    (hCsmall : C ≤ L / 10000) (hBsmall : B ≤ L / 10000)
    (hEsmall : E ≤ L / 10000) (ht : t ≤ 1 / 11) :
    (3 / 100 : ℝ) * L ≤ (L / 10 - C - B) / 2 - t * (L / 5 + C) - E := by
…

theorem OAI.Ostmann.split_prime_mass_of_small_errors line 47

Source documentation

Specialization of the proved split mass, with no prime-sum hypothesis.

theorem split_prime_mass_of_small_errors (d : ℤ) (D Q Y : ℕ)
    (L C B : ℝ) (hL : 0 < L) (hQ : 0 < Q) (hC : 0 ≤ C)
    (hCsmall : C ≤ L / 10000) (hBsmall : B ≤ L / 10000)
    (hEsmall : (Y : ℝ) + Real.log D / Y ≤ L / 10000)
    (hlog : (12 / 25 : ℝ) * L ≤ Real.log (Q : ℝ))
    (hmass : (1 / ((1 + 10 / L) - 1) - C - B) / 2 -
      (Q : ℝ) ^ (-((1 + 10 / L) - 1) / 2) * (2 / ((1 + 10 / L) - 1) + C) -
      (Y + Real.log D / Y) ≤
      ∑ p ∈ (Nat.primesLE Q).filter (fun p => ¬p ∣ D ∧ jacobiSym d p = 1),
        Real.log p / (p : ℝ)) :
    (3 / 100 : ℝ) * L ≤
      ∑ p ∈ (Nat.primesLE Q).filter (fun p => ¬p ∣ D ∧ jacobiSym d p = 1),
…