Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.tendsto_deriv_kernel_second_ibp_limit

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2977 to 3005

Mathematical statement

Exact Lean statement

lemma tendsto_deriv_kernel_second_ibp_limit {a b : ℝ} (ha : 0 < a) (hab : a < b)
    (s : ℂ) :
    Tendsto
      (fun N : ℕ ↦
        ∑ n ∈ range N,
          ∫ y in a..b,
            deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y *
              ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /
                (Real.pi * (n + 1 : ℝ))) : ℂ))
      atTop
      (𝓝
        (deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b *
            (((-(Int.fract b ^ 2 - Int.fract b + 1 / 6) / 2) : ℝ) : ℂ) -
          deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a *
            (((-(Int.fract a ^ 2 - Int.fract a + 1 / 6) / 2) : ℝ) : ℂ) -
          ∫ y in a..b,
            (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *
              (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_deriv_kernel_second_ibp_limit {a b : ℝ} (ha : 0 < a) (hab : a < b)    (s : ℂ) :    Tendsto      (fun N : ℕ ↦        ∑ n ∈ range N,          ∫ y in a..b,            deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y *              ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /                (Real.pi * (n + 1 : ℝ))) : ℂ))      atTop      (𝓝        (deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b *            (((-(Int.fract b ^ 2 - Int.fract b + 1 / 6) / 2) : ℝ) : ℂ) -          deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a *            (((-(Int.fract a ^ 2 - Int.fract a + 1 / 6) / 2) : ℝ) : ℂ) -          ∫ y in a..b,            (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *              (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ))) := by  have hb :=    (tendsto_cos_antideriv_partial b).const_mul      (deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b)  have ha_tendsto :=    (tendsto_cos_antideriv_partial a).const_mul      (deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a)  have hint := (hasSum_second_ibp_integral_series (a := a) (b := b) ha hab s).tendsto_sum_nat  have hcombined := (hb.sub ha_tendsto).sub hint  refine hcombined.congr' ?_  filter_upwards with N  exact (deriv_kernel_partial_sum_second_ibp (a := a) (b := b) ha hab s N).symm