PrimeBilinearReduction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Reducing a prime bilinear sum to its rational-frequency kernel

theorem OAI.JointDickman.prime_bilinear_kernel_bound line 13

Source documentation

The finite smoothed estimate before the rational-frequency summation. The width X bounds only the prime differences; Q bounds the prime locations.

theorem prime_bilinear_kernel_bound : ∃ C : ℝ, 0 < C ∧
    ∀ (Q X Y : ℕ) (P : Finset ℕ) (b : ℕ → ℂ) (c : ℤ → ℂ) (θ : ℝ) (a : ℤ),
    2 ≤ Q → (∀ p ∈ P, p.Prime ∧ p ≤ Q) →
    (∀ p ∈ P, ∀ r ∈ P, r-p ≤ X) →
    (∀ p ∈ P, ‖b p‖ ≤ Real.log Q) →
    (∀ n ∈ Ico a (a+Y), ‖c n‖ ≤ 1) →
    ‖∑ n ∈ Ico a (a+Y), c n * ∑ p ∈ P, b p * additivePhase (θ*p*n)‖^2 ≤
      C*((Q:ℝ)*Real.log Q*(Y:ℝ)^2 + (Q:ℝ)*
        ∑ h ∈ Icc 1 X, ((h:ℝ)/h.totient)*geometricSquareKernel (2*Y) (θ*h)) := by
…

Mentions: OAI.JointDickman.additivePhase, OAI.JointDickman.geometricSquareKernel