MajorArcRational.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Resolving a rational additive phase into its residue classes before the multiplicative character expansion. Only a factor equal to the modulus is lost; no Gauss-sum estimate is needed for the application.

lemma OAI.TwoPointCorrelations.major_arc_rational_character line 15
lemma OAI.TwoPointCorrelations.major_arc_residue_partition line 24
lemma OAI.TwoPointCorrelations.major_arc_rational_sum_norm line 44

theorem OAI.TwoPointCorrelations.major_arc_typical_rational_bound line 56

Source documentation

A common bound for the reduced, twisted intervals controls the rational frequency with the exact modulus loss.

theorem major_arc_typical_rational_bound {ι : Type*} (J : Finset ι)
    (P : ι → Finset ℕ) (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime)
    (F : ℕ → ℂ)
    (hF : ∀ a b, 0 < a → 0 < b → F (a * b) = F a * F b)
    (hFb : OneBounded F) (q X H : ℕ) [NeZero q] (r : ℤ) (K : ℝ)
    (havoid : ∀ b : ZMod q, mrtPrimeAvoids (J.biUnion P) (b.val.gcd q))
    (hK : ∀ (b : ZMod q) (χ : DirichletCharacter ℂ (q / b.val.gcd q)),
      (b.val.gcd q : ℝ) * shortExponentialIntegral
        (mrtTypicalCoefficient J P (twistByCharacter F χ))
        (X / b.val.gcd q + 1) (H / b.val.gcd q + 1) 0 + X ≤ K) :
    shortExponentialIntegral (mrtTypicalCoefficient J P F) X H ((r : ℝ) / q) ≤
      (q : ℝ) * K := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtPrimeAvoids, OAI.TwoPointCorrelations.shortExponentialIntegral, OAI.TwoPointCorrelations.mrtTypicalCoefficient, OAI.TwoPointCorrelations.twistByCharacter