A362583

Part of: Dirichlet series with bounded partial sums: the by-parts series is the analytic continuation to the right half-plane.

DefinitionbpSeries

The by-parts series of f : \mathbb{N} \to \C is \tilde A_f(s) \;=\; \sum_{n \ge 0} \Bigl(\sum_{k \le n} f(k)\Bigr)\bigl(n^{-s} - (n+1)^{-s}\bigr). It is what discrete Abel summation produces from the Dirichlet series \sum_n f(n)\, n^{-s}, but here it is taken as the definition of the continuation object. No hypothesis on f(0) is needed anywhere: Lean's junk value 0^{-s} = 0 (for s \ne 0) makes the n = 0 term harmless, and the identification below is exact as stated.

Lean code for Definition bpSeries
  • ⟲
    def bpSeries (fℕ → ℂ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) (sℂ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.  
    def bpSeries (fℕ → ℂ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
 → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) (sℂ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.  
⟲:= ∑' nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
, (∑ kℕ ∈ Finset.rangeFinset.range (n : ℕ) : Finset ℕ`range n` is the set of natural numbers less than `n`.  (nℕ + 1ℕ), fℕ → ℂ kℕ) * ((nℕ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ) - ((nℕ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) + 1ℂ) ^ (-sℂ))

Local dependency graph