OAI/NumberTheory/Ostmann/ZeroDensity/SchwartzDensityCorrelation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.correlationWeightBudget line 12
2. theorem OAI.Ostmann.schwartz_density_correlation_bound line 20

   Source documentation

   Each expanded pair is bounded by its exact exclusive-prime factor times the interval length and a fixed Schwartz seminorm budget.

   theorem schwartz_density_correlation_bound (ps qs rs : List ℕ)
       (hp : ∀ p ∈ ps, p.Prime) (hq : ∀ p ∈ qs, p.Prime) (hr : ∀ p ∈ rs, p.Prime)
       (hcp : ps.Pairwise Nat.Coprime) (hcq : qs.Pairwise Nat.Coprime) (hcr : rs.Pairwise Nat.Coprime)
       (hrs : rs.toFinset = ps.toFinset ∪ qs.toFinset)
       (vp : (ZMod ps.prod)ˣ) (vq : (ZMod qs.prod)ˣ)
       (f : ∀ p : ℕ, ZMod p → ℂ) (hf : ∀ p ∈ rs, ∀ x, ‖f p x‖ ≤ 1)
       (Φ Ψ : 𝓢(ℝ, ℂ)) (α β Y Z C D : ℝ) (M N : ℕ)
       (hY : 0 < Y) (hZ : 0 < Z) (hNY : (N : ℝ) ≤ C * Y) (hNZ : (N : ℝ) ≤ D * Z)
       (hN : rs.prod ^ 2 ≤ N) :
       let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
   …

   Mentions: OAI.Ostmann.prime_list_prod_pos