OddJacobiMoment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An explicit Bonami moment bound over all odd moduli

theorem OAI.Ostmann.odd_jacobi_even_moment_bound line 13

Source documentation

The nonsquare contribution is bounded by 8*U^(2*l) independently of how many moduli are summed. Only the classical Bonami input remains.

theorem odd_jacobi_even_moment_bound (hB : PublishedBonamiBound)
    (P S : Finset ℕ) (hS : ∀ s ∈ S, Squarefree s)
    (hP : ∀ s ∈ S, s.primeFactors ⊆ P) (U M l : ℕ)
    (hU : ∀ s ∈ S, s ≤ U) (hl : 0 < l) (a : S → ℝ) :
    (∑ m ∈ Finset.range M, if Odd m then
        |∑ s : S, a s * realJacobi s.val m| ^ (2 * l) else 0) ≤
      (M : ℝ) *
        (∑ s : S, ((2 * l - 1 : ℕ) : ℝ) ^ s.val.primeFactors.card * |a s| ^ 2) ^ l +
      (8 * (U : ℝ) ^ (2 * l)) * (∑ s : S, |a s|) ^ (2 * l) := by
…

Mentions: OAI.Ostmann.PublishedBonamiBound, OAI.Ostmann.realJacobi