OAI/NumberTheory/Ostmann/Quadratic/QuadraticSplitMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.jacobi_ne_zero_of_prime_not_dvd line 11
2. theorem OAI.Ostmann.quadratic_split_mass_bound line 19

   Source documentation

   All losses are expressed in the original nonnegative weights. In the application w(p)=log(p)/p^s, and the removed divisor is 2*m*abs(d).

   theorem quadratic_split_mass_bound (P : Finset ℕ) (d : ℤ) (D Q : ℕ)
       (hdD : d.natAbs ∣ D) (hP : ∀ p ∈ P, p.Prime) (w : ℕ → ℝ)
       (hw : ∀ p ∈ P, 0 ≤ w p) (L B T E : ℝ)
       (htotal : L ≤ ∑ p ∈ P, w p)
       (hsigned : -B ≤ ∑ p ∈ P, w p * (jacobiSym d p : ℝ))
       (htail : (∑ p ∈ P.filter (fun p => Q < p), w p) ≤ T)
       (hdiv : (∑ p ∈ P.filter (fun p => p ∣ D), w p) ≤ E) :
       (L - B) / 2 - T - E ≤
         ∑ p ∈ P.filter (fun p => p ≤ Q ∧ ¬p ∣ D ∧ jacobiSym d p = 1), w p := by
   …