OAI/NumberTheory/Ostmann/QuadraticSieve/WeightedJacobiMoment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transferring square-product moments to weighted Jacobi sums

The nonsquare error is an explicit numerical bound to be supplied by the periodic-character calculation; it is not a published or global assumption.

  1. def OAI.Ostmann.realJacobi line 16
  2. theorem OAI.Ostmann.realJacobi_abs_le line 18
  3. theorem OAI.Ostmann.realJacobi_prod line 21
  4. theorem OAI.Ostmann.weighted_jacobi_abs_le_mass line 29
  5. theorem OAI.Ostmann.weighted_jacobi_moment_expansion line 38
  6. theorem OAI.Ostmann.weighted_jacobi_even_moment_bound line 53

    Source documentation

    Bonami controls the square products. Every remaining product pays only the supplied finite nonsquare-character error E.

    theorem weighted_jacobi_even_moment_bound (hB : PublishedBonamiBound)
    (P S T : Finset ℕ) (hS : ∀ s ∈ S, Squarefree s)
    (hP : ∀ s ∈ S, s.primeFactors ⊆ P) (μ : ℕ → ℝ)
    (hμ : ∀ m ∈ T, 0 ≤ μ m) (a : S → ℝ) (l : ℕ) (hl : 0 < l)
    (E : ℝ) (hE : 0 ≤ E)
    (hns : ∀ t : Fin (2 * l) → S, ¬IsSquare (∏ j, (t j).val) →
      |∑ m ∈ T, μ m * realJacobi (∏ j, (t j).val) m| ≤ E) :
    (∑ m ∈ T, μ m * |∑ s : S, a s * realJacobi s.val m| ^ (2 * l)) ≤
      (∑ m ∈ T, μ m) *
        (∑ s : S, ((2 * l - 1 : ℕ) : ℝ) ^ s.val.primeFactors.card * |a s| ^ 2) ^ l +
      E * (∑ s : S, |a s|) ^ (2 * l) := by
…

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