OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSmoothTypical.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth Dirichlet series restricted to the typical set. Finite inclusion-exclusion and the proved smooth Euler formula give the exact product of nonempty-band Euler factors.

  1. def OAI.TwoPointCorrelations.mrtMaskedCoefficient line 15
  2. lemma OAI.TwoPointCorrelations.mrtMaskedCoefficient_one line 18
  3. lemma OAI.TwoPointCorrelations.mrtMaskedCoefficient_mul line 22
  4. lemma OAI.TwoPointCorrelations.mrtMaskedCoefficient_oneBounded line 31
  5. lemma OAI.TwoPointCorrelations.mrtMaskedCoefficient_term line 38
  6. theorem OAI.TwoPointCorrelations.mrt_masked_smooth_euler line 46
  7. theorem OAI.TwoPointCorrelations.mrt_typical_smooth_euler line 71

    Source documentation

    Exact equation (A.11) before taking norms: the typical smooth series equals a complement Euler product times the nonempty-band factors.

    theorem mrt_typical_smooth_euler {ι : Type*} (F : ℕ → ℂ) (hF1 : F 1 = 1)
    (hF : ∀ m n, 0 < m → 0 < n → F (m * n) = F m * F n)
    (hFb : OneBounded F) (N : ℕ) (t : ℝ) (J : Finset ι) (P : ι → Finset ℕ)
    (hP : ∀ j ∈ J, P j ⊆ primesUpTo N) (hdis : Set.PairwiseDisjoint (J : Set ι) P) :
    HasSum (fun n : Nat.smoothNumbers (N + 1) =>
      if mrtTypical J P n then LSeries.term F (1 + (t : ℂ) * Complex.I) n else 0)
      ((∏ p ∈ primesUpTo N \ J.biUnion P, (1 - mrtPrimeEulerTerm F t p)⁻¹) *
        ∏ j ∈ J, ((∏ p ∈ P j, (1 - mrtPrimeEulerTerm F t p)⁻¹) - 1)) := by
…

    Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.primesUpTo, OAI.TwoPointCorrelations.mrtTypical, OAI.TwoPointCorrelations.mrtPrimeEulerTerm