JacobiFamilyMoment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A moment bound uniform over a finite family of coefficient arrays

theorem OAI.Ostmann.complex_odd_jacobi_chosen_moment_bound line 13

Source documentation

The array may be chosen separately at each modulus. Thus this estimate also bounds the pointwise maximum over the family.

theorem complex_odd_jacobi_chosen_moment_bound (hB : PublishedBonamiBound)
    {I : Type*} [Fintype I] (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)
    (b : I → S → ℂ) (pick : ℕ → I) (E A : ℝ)
    (henergy : ∀ i, (∑ s : S, ((2 * l - 1 : ℕ) : ℝ) ^ s.val.primeFactors.card * ‖b i s‖ ^ 2) ≤ E)
    (hmass : ∀ i, (∑ s : S, ‖b i s‖) ≤ A) :
    (∑ m ∈ Finset.range M, if Odd m then
        ‖∑ s : S, b (pick m) s * (realJacobi s.val m : ℂ)‖ ^ (2 * l) else 0) ≤
      (Fintype.card I : ℝ) * (2 : ℝ) ^ (2 * l) *
        ((M : ℝ) * E ^ l + (8 * (U : ℝ) ^ (2 * l)) * A ^ (2 * l)) := by
…

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