Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.tendsto_deriv_kernel_to_neg_B1

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3436 to 3451

Mathematical statement

Exact Lean statement

lemma tendsto_deriv_kernel_to_neg_B1 {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
      (𝓝 (-(∫ y in a..b,
        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * B1 y)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_deriv_kernel_to_neg_B1 {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      (𝓝 (-(∫ y in a..b,        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * B1 y))) := by  have hlim := tendsto_deriv_kernel_second_ibp_limit (a := a) (b := b) ha hab s  have hidentity := secondIBPExpr_eq_negB1IntegralExpr (a := a) (b := b) ha hab.le s  refine hlim.trans_eq ?_  simpa [secondIBPExpr, negB1IntegralExpr, bernoulli2Primitive] using hidentity