Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.kadiri_thm_3_1_q1_shifted_eq_I123

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1163 to 1203

Mathematical statement

Exact Lean statement

@[blueprint
  "kadiri-thm-3-1-q1-shifted-eq-I123"
  (title := "Functional-equation decomposition of the $\\sigma = -a$ integral")
  (statement := /-- Under the hypotheses of \ref{kadiri-thm-3-1-q1-eq-11}: for every
  $T > 0$,
  $$ \frac{1}{2\pi i} \int_{-a - iT}^{-a + iT}
       \!\!\!\! \left(-\frac{\zeta'}{\zeta}\right)\!(s)\, \Phi(-s)\, ds
     \;=\; I_1(T) + I_2(T) + I_3(T), $$
  where $I_1, I_2, I_3$ are the three pieces produced by applying
  \ref{kadiri-thm-3-1-q1-functional-eq} to the integrand. -/)
  (proof := /-- Apply \ref{kadiri-thm-3-1-q1-functional-eq} pointwise inside the
  integral. The hypotheses of the functional equation hold on the entire contour
  $\sigma = -a$: $s = -a + it \neq 1$ (since $\Re s = -a \leq 0$), $s \neq 0$ (since
  $a > 0$), $s \notin Z(\zeta)$ (since $\Re s = -a < 0$ but non-trivial zeros have
  $\Re \rho \in (0, 1)$), and $1 - s \notin Z(\zeta)$ (since $\Re(1 - s) = 1 + a > 1$).
  Linearity of the integral splits it into the three pieces of the definitions of
  $I_1, I_2, I_3$. To be formalised. -/)
  (latexEnv := "sublemma")
  (discussion := 1541)]
theorem kadiri_thm_3_1_q1_shifted_eq_I123
    {φ : ℝ → ℂ} (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) (T : ℝ) :
    let Φ : ℂ → ℂ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "kadiri-thm-3-1-q1-shifted-eq-I123"  (title := "Functional-equation decomposition of the $\\sigma = -a$ integral")  (statement := /-- Under the hypotheses of \ref{kadiri-thm-3-1-q1-eq-11}: for every  $T > 0$,  $$ \frac{1}{2\pi i} \int_{-a - iT}^{-a + iT}       \!\!\!\! \left(-\frac{\zeta'}{\zeta}\right)\!(s)\, \Phi(-s)\, ds     \;=\; I_1(T) + I_2(T) + I_3(T), $$  where $I_1, I_2, I_3$ are the three pieces produced by applying  \ref{kadiri-thm-3-1-q1-functional-eq} to the integrand. -/)  (proof := /-- Apply \ref{kadiri-thm-3-1-q1-functional-eq} pointwise inside the  integral. The hypotheses of the functional equation hold on the entire contour  $\sigma = -a$: $s = -a + it \neq 1$ (since $\Re s = -a \leq 0$), $s \neq 0$ (since  $a > 0$), $s \notin Z(\zeta)$ (since $\Re s = -a < 0$ but non-trivial zeros have  $\Re \rho \in (0, 1)$), and $1 - s \notin Z(\zeta)$ (since $\Re(1 - s) = 1 + a > 1$).  Linearity of the integral splits it into the three pieces of the definitions of  $I_1, I_2, I_3$. To be formalised. -/)  (latexEnv := "sublemma")  (discussion := 1541)]theorem kadiri_thm_3_1_q1_shifted_eq_I123    {φ : ℝ → ℂ} (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) (T : ℝ) :    let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume    (1 / (2 * (Real.pi : ℂ))) *      (∫ t in Set.Ioo (-T) T,        (-deriv riemannZeta (((-a : ℝ) : ℂ) + (t : ℂ) * I) /            riemannZeta (((-a : ℝ) : ℂ) + (t : ℂ) * I)) *          Φ (-(((-a : ℝ) : ℂ) + (t : ℂ) * I))) =      kadiri_thm_3_1_q1_I_1 φ a T      + kadiri_thm_3_1_q1_I_2 φ a T      + kadiri_thm_3_1_q1_I_3 φ a T := by  have hΦ := kadiri_laplace_shifted_vertical_segment_continuousOn    (φ := φ) hφ hb hφ_decay ha hab ha1 (T := T)  exact kadiri_thm_3_1_q1_shifted_eq_I123_of_transform_continuous ha ha1 hΦ    (u1541_shifted_I1_summand_integrable_of_transform_continuous hΦ)    (u1541_shifted_I2_summand_integrable_of_transform_continuous ha hΦ)