MRTTypicalEulerBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact typical smooth Euler product retains half of the full pretentious-distance exponent, independently of the number of bands.

theorem OAI.TwoPointCorrelations.mrt_typical_smooth_euler_bound line 14

theorem OAI.TwoPointCorrelations.mrt_typical_smooth_distance_bound line 59

Source documentation

The absolute constant does not depend on the number or positions of the disjoint prime bands.

theorem mrt_typical_smooth_distance_bound : ∃ C : ℝ, 0 < C ∧
    ∀ (F : ℕ → ℂ), F 1 = 1 →
      (∀ m n, 0 < m → 0 < n → F (m * n) = F m * F n) → OneBounded F →
      ∀ (N : ℕ), 2 ≤ N → ∀ (t : ℝ) {ι : Type*} (J : Finset ι) (P : ι → Finset ℕ),
      (∀ j ∈ J, P j ⊆ primesUpTo N) → Set.PairwiseDisjoint (J : Set ι) P →
      ‖∑' n : Nat.smoothNumbers (N + 1),
        if mrtTypical J P n then LSeries.term F (1 + (t : ℂ) * Complex.I) n else 0‖ ≤
        C * Real.log N * Real.exp (-squaredDistance F (mrtArchimedeanTwist t) N / 2) := by
…

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