Kadiri.kadiri_thm_3_1_q1_eq_11_truncated_limit_of_pointwise_inversion
PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:880 to 914
Source documentation
The faithful truncated-limit form of Kadiri equation (11) (\cite{Kadiri2005},
Théorème 3.1, eq.~(11), arXiv math/0401238): the von Mangoldt sum is the T → ∞
limit of the truncated contour integral kadiri_thm_3_1_q1_I φ a T over the compact
segment [1+a-iT, 1+a+iT]. Under the same C¹ hypotheses as the stub
kadiri_thm_3_1_q1_eq_11, the only remaining analytic input is the single-point
truncated-limit Laplace inversion hinv (the displayed identity just before
\cite[(11)]{Kadiri2005}); the sum/integral exchange over the compact window and the
Tannery domination are discharged by this file, so no full-line L¹ integrability is
needed. This replaces the (mis-stated) absolute Bochner form ∫ t : ℝ of the stub.
Exact Lean statement
theorem kadiri_thm_3_1_q1_eq_11_truncated_limit_of_pointwise_inversion
{φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)
{b : ℝ} (hb : 0 < b)
(hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))
=O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))
(hφ'_decay : (fun x : ℝ ↦ deriv φ x * exp ((x : ℂ) / 2))
=O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))
{a : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : a < 1)
(hinv : ∀ n : Nat, 1 ≤ n →
let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume
Tendsto
(fun T : ℝ =>
(1 / (2 * (Real.pi : ℂ))) *
∫ t in (-T)..T,
Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *
(n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))
atTop (𝓝 (φ (Real.log n)))) :
Tendsto (fun T : ℝ => kadiri_thm_3_1_q1_I φ a T) atTop
(𝓝 (∑' n : ℕ, (Λ n : ℂ) * φ (Real.log n)))Complete declaration
Lean source
theorem kadiri_thm_3_1_q1_eq_11_truncated_limit_of_pointwise_inversion {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ) {b : ℝ} (hb : 0 < b) (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2)) =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) (hφ'_decay : (fun x : ℝ ↦ deriv φ x * exp ((x : ℂ) / 2)) =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) {a : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : a < 1) (hinv : ∀ n : Nat, 1 ≤ n → let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume Tendsto (fun T : ℝ => (1 / (2 * (Real.pi : ℂ))) * ∫ t in (-T)..T, Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) * (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) atTop (𝓝 (φ (Real.log n)))) : Tendsto (fun T : ℝ => kadiri_thm_3_1_q1_I φ a T) atTop (𝓝 (∑' n : ℕ, (Λ n : ℂ) * φ (Real.log n))) := by -- The bank reduction gives the limit for the interval-integral form `∫ t in (-T)..T`. have hbank := kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion (φ := φ) hφ (b := b) hb hφ_decay hφ'_decay (a := a) ha hab ha1 hinv dsimp only at hbank -- `kadiri_thm_3_1_q1_I` uses `∫ t in Set.Ioo (-T) T`; the bank uses `∫ t in (-T)..T`. -- For `T ≥ 0` these set integrals agree (`(-T)..T = Ioc (-T) T`, and `Ioo`/`Ioc` -- differ only on the null set `{T}`), so the two limits coincide eventually. refine hbank.congr' ?_ filter_upwards [Filter.eventually_ge_atTop (0 : ℝ)] with T hT have hTle : (-T) ≤ T := by linarith unfold kadiri_thm_3_1_q1_I dsimp only congr 1 rw [intervalIntegral.integral_of_le hTle, MeasureTheory.integral_Ioc_eq_integral_Ioo]