MajorArcResidues.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Gcd reduction of a typical-set progression, including nonunit classes. The removed gcd avoids the prime bands, so the typical mask is unchanged. The resulting windows are literal character twists at the divided scale.

lemma OAI.TwoPointCorrelations.major_arc_typical_dilation line 16

lemma OAI.TwoPointCorrelations.major_arc_typical_residue_identity line 37

Source documentation

The original residue b is unrestricted; the reduced character modulus is q / gcd b q, and this also covers reduced modulus one.

lemma major_arc_typical_residue_identity {ι : 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)
    (q b : ℕ) (hq : 0 < q)
    (havoid : mrtPrimeAvoids (J.biUnion P) (b.gcd q))
    {n : ℕ} (hn : 0 < n) :
    (if n % q = b % q then mrtTypicalCoefficient J P F n else 0) =
      F (b.gcd q) * ((q / b.gcd q).totient : ℂ)⁻¹ *
        ∑ χ : DirichletCharacter ℂ (q / b.gcd q),
          conj (naturalCharacter χ (b / b.gcd q)) *
            dilationSequence (b.gcd q)
…

Mentions: OAI.TwoPointCorrelations.mrtPrimeAvoids, OAI.TwoPointCorrelations.mrtTypicalCoefficient, OAI.TwoPointCorrelations.naturalCharacter, OAI.TwoPointCorrelations.dilationSequence

lemma OAI.TwoPointCorrelations.major_arc_typical_residue_window line 65
lemma OAI.TwoPointCorrelations.major_arc_typical_residue_window_norm line 90
lemma OAI.TwoPointCorrelations.major_arc_dilation_average line 115

theorem OAI.TwoPointCorrelations.major_arc_typical_residue_average line 136

Source documentation

Averaging all original origins costs the gcd exactly once. The only rounding error is one endpoint per origin.

theorem major_arc_typical_residue_average {ι : 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 b X H : ℕ) (hq : 0 < q)
    (havoid : mrtPrimeAvoids (J.biUnion P) (b.gcd q)) :
    (∑ v ∈ range X, ‖∑ n ∈ Icc (v + 1) (v + H),
      if n % q = b % q then mrtTypicalCoefficient J P F n else 0‖) ≤
      ((q / b.gcd q).totient : ℝ)⁻¹ *
        ∑ χ : DirichletCharacter ℂ (q / b.gcd q),
          ((b.gcd q : ℝ) * shortExponentialIntegral
            (mrtTypicalCoefficient J P (twistByCharacter F χ))
…

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