QuadraticDensityCorrelation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The large-kernel correlation of the original centered-density quadratic sums

theorem OAI.Ostmann.quadratic_density_correlation_bound line 15

Source documentation

This is the finite, explicit form of the manuscript's correlation (src12). The cutoff hypotheses give both the support pair count and smooth scaling; all Fourier and nonunit conditions are supplied by the centered densities.

theorem quadratic_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)
    (S : ∀ p : ℕ, Finset (ZMod p)) (W V : Finset ℕ)
    (a : ZMod ps.prod) (b : ZMod qs.prod) (Φ Ψ : 𝓢(ℝ, ℂ))
    (θ η R v C : ℝ) (M N : ℕ) (hR : 0 < R) (hv : 0 < v) (hC : 0 ≤ C)
    (hM : 0 < M) (hN : 0 < N) (hperiod : rs.prod ^ 2 ≤ N)
    (hW : ∀ w ∈ W, 0 < w ∧ (w : ℝ) ^ 2 ≤ C * R * ps.prod / ((N : ℝ) * v))
    (hV : ∀ w ∈ V, 0 < w ∧ (w : ℝ) ^ 2 ≤ C * R * qs.prod / ((N : ℝ) * v)) :
    let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
…

Mentions: OAI.Ostmann.prime_list_prod_pos