Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.deriv_kernel_partial_sum_second_ibp

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2836 to 2889

Mathematical statement

Exact Lean statement

lemma deriv_kernel_partial_sum_second_ibp {a b : ℝ} (ha : 0 < a) (hab : a < b)
    (s : ℂ) (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 : ℝ))) : ℂ) =
      deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b *
          (∑ n ∈ range N,
            ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * b) /
              (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)) -
        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a *
          (∑ n ∈ range N,
            ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * a) /
              (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)) -
        ∑ n ∈ range N,
          ∫ y in a..b,
            (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *
              ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) /
                (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma deriv_kernel_partial_sum_second_ibp {a b : ℝ} (ha : 0 < a) (hab : a < b)    (s : ℂ) (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 : ℝ))) : ℂ) =      deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b *          (∑ n ∈ range N,            ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * b) /              (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)) -        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a *          (∑ n ∈ range N,            ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * a) /              (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)) -        ∑ n ∈ range N,          ∫ y in a..b,            (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *              ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) /                (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ) := by  calc    ∑ 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 : ℝ))) : ℂ)        = ∑ n ∈ range N,          (deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b *              ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * b) /                (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ) -            deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a *              ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * a) /                (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ) -            ∫ y in a..b,              (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *                ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) /                  (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)) := by          apply sum_congr rfl          intro n _hn          exact deriv_kernel_integral_by_parts_cpow ha hab s n    _ = deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b *          (∑ n ∈ range N,            ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * b) /              (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)) -        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a *          (∑ n ∈ range N,            ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * a) /              (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)) -        ∑ n ∈ range N,          ∫ y in a..b,            (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *              ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) /                (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ) := by          simp [sum_sub_distrib, mul_sum]