OAI/NumberTheory/Ostmann/QuadraticCenter/PrimeSetQuadratic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.primeSet_list_prime line 13
2. theorem OAI.Ostmann.primeSet_list_coprime line 16
3. def OAI.Ostmann.primeSetQuadraticSum line 23
4. theorem OAI.Ostmann.support_correlation_product line 31
5. theorem OAI.Ostmann.primeSet_prod_le_of_subset line 53
6. theorem OAI.Ostmann.primeSet_prod_dvd_of_subset line 61
7. theorem OAI.Ostmann.primeSetQuadraticSum_eq_unit_waves line 65
8. theorem OAI.Ostmann.primeSet_quadratic_correlation line 83

   Source documentation

   The pair bound for actual prime-divisor sums, with the common modulus and exclusive-prime factor obtained from their prime sets.

   theorem primeSet_quadratic_correlation (P U V : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (hU : U ⊆ P) (hV : V ⊆ P)
       (S : ∀ p : ℕ, Finset (ZMod p)) (W Vw : Finset ℕ)
       (a : ZMod U.toList.prod) (b : ZMod V.toList.prod) (Φ Ψ : 𝓢(ℝ, ℂ))
       (θ η R v C : ℝ) (M N : ℕ) (hR : 0 < R) (hv : 0 < v) (hC : 0 ≤ C)
       (hM : 0 < M) (hN : 0 < N) (hperiod : P.toList.prod ^ 2 ≤ N)
       (hW : ∀ w ∈ W, 0 < w ∧ (w : ℝ) ^ 2 ≤ C * R * U.toList.prod / ((N : ℝ) * v))
       (hVw : ∀ w ∈ Vw, 0 < w ∧ (w : ℝ) ^ 2 ≤ C * R * V.toList.prod / ((N : ℝ) * v)) :
       ‖∑ n ∈ Finset.range N,
         primeSetQuadraticSum U (fun p hp => hP p (hU hp)) S W a θ Φ R v (n + M) *
         conj (primeSetQuadraticSum V (fun p hp => hP p (hV hp)) S Vw b η Ψ R v (n + M)) /
           ((n + M : ℕ) : ℂ)‖ ≤
   …

   Mentions: OAI.Ostmann.primeSetQuadraticSum