AmplifiedCharacterPoisson.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Poisson transfer of the original amplified character sum

theorem OAI.Ostmann.bounded_schwartz_lattice_summable line 13
theorem OAI.Ostmann.norm_jacobiComplex_int_le line 24
theorem OAI.Ostmann.primeDivisorDensity_norm line 27
theorem OAI.Ostmann.amplified_jacobi_poisson line 36

theorem OAI.Ostmann.amplified_jacobi_positive_bound line 89

Source documentation

The actual amplified physical sum is controlled by the original positive Fourier statistic with its exact square-root scale.

theorem amplified_jacobi_positive_bound (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime)
    (D : ∀ p : ℕ, Finset (ZMod p)) (M N h₀ : ℕ) [NeZero M]
    (hcop : Q.toList.prod.Coprime M) (hM : Squarefree M) (hodd : Odd M) (hM1 : 1 < M)
    (t : ZMod M) (hlift : (Q.toList.prod : ℤ) ∣ (t.val : ℤ) + (M : ℤ) * h₀)
    (ψ : 𝓢(ℝ, ℂ)) (hreal : ∀ x, conj (ψ x) = ψ x) (X H : ℝ) (hX : 0 < X)
    (hH : 0 ≤ H) (hcut : H * ((M : ℝ) / X) * Q.toList.prod ≤ N)
    (hsupp : ∀ x : ℝ, H < x → 𝓕 ψ x = 0) :
    ‖∑' n : ℤ, (amplificationWeight Q D n : ℂ) *
        (jacobiSym (n - t.val) M : ℂ) * ψ ((n : ℝ) / X)‖ ≤
      2 * Real.sqrt X *
        ‖originalPositiveFourier Q hQ D M N h₀ ((t.val : ℝ) / M) ((M : ℝ) / X) (𝓕 ψ)‖ := by
…

Mentions: OAI.Ostmann.amplificationWeight, OAI.Ostmann.originalPositiveFourier