Theorem exp_layers_eq

Part of: The k = 1 layer, the split of the Euler-product logarithm into layers, the identity exp(A + B + T) = L(s, χ), and the coefficient bridge to the race sum.

Theoremexp_layers_eq_LFunction

Euler wiring. For \mathrm{Re}\, s > 1, \exp\bigl(A(s) + B(s) + T(s)\bigr) \;=\; L(s, \chi), where L is Mathlib's analytically continued Dirichlet L-function of \chi — an entire function, since \chi is nonprincipal. From here on, "the L-function" always means this continued object; its two properties used later are entirety (hence continuity at 1/2) and nonvanishing at s = 1.

Lean code for Theorem exp_layers_eq_LFunction

⟲

theorem exp_layers_eq_LFunction {sℂ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } (hs1 < s.re : 1ℝ < sℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. ) :
    Complex.expComplex.exp (z : ℂ) : ℂThe complex exponential function, defined via its Taylor series  (layerAA362583.layerA (s : ℂ) : ℂThe `k = 1` layer `A(s) = Σ_p χ(p) p^(-s)`.  sℂ + layerBA362583.layerB (s : ℂ) : ℂThe `k = 2` layer `B(s) = (1/2) Σ_{p odd} p^(-2s)`, with an `if`-mask at
`p = 2` (`χ(2)² = 0`, `χ(p)² = 1` for odd `p`; see `χ_sq_eq_ite`,
`tsum_term_two_eq_layerB`).  Exponent convention: `-(2 * s)`.  sℂ + layerTA362583.layerT (s : ℂ) : ℂThe `k ≥ 3` layer `T(s) = Σ_p t_p(s)`.  sℂ) = DirichletCharacter.LFunctionDirichletCharacter.LFunction {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ) : ℂThe unique meromorphic function `ℂ → ℂ` which agrees with `∑' n : ℕ, χ n / n ^ s` wherever the
latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions.

Note that this is not the same as `LSeries χ`: they agree in the convergence range, but
`LSeries χ s` is defined to be `0` if `re s ≤ 1`.
 χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  sℂ

theorem exp_layers_eq_LFunction {sℂ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } (hs1 < s.re : 1ℝ < sℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. ) :
    Complex.expComplex.exp (z : ℂ) : ℂThe complex exponential function, defined via its Taylor series  (layerAA362583.layerA (s : ℂ) : ℂThe `k = 1` layer `A(s) = Σ_p χ(p) p^(-s)`.  sℂ + layerBA362583.layerB (s : ℂ) : ℂThe `k = 2` layer `B(s) = (1/2) Σ_{p odd} p^(-2s)`, with an `if`-mask at
`p = 2` (`χ(2)² = 0`, `χ(p)² = 1` for odd `p`; see `χ_sq_eq_ite`,
`tsum_term_two_eq_layerB`).  Exponent convention: `-(2 * s)`.  sℂ + layerTA362583.layerT (s : ℂ) : ℂThe `k ≥ 3` layer `T(s) = Σ_p t_p(s)`.  sℂ) = DirichletCharacter.LFunctionDirichletCharacter.LFunction {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ) : ℂThe unique meromorphic function `ℂ → ℂ` which agrees with `∑' n : ℕ, χ n / n ^ s` wherever the
latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions.

Note that this is not the same as `LSeries χ`: they agree in the convergence range, but
`LSeries χ s` is defined to be `0` if `re s ≤ 1`.
 χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  sℂ

By the layer split, A(s) + B(s) + T(s) = \sum_p -\operatorname{Log}(1 - \chi(p)\, p^{-s}). Exponentiating, Mathlib's exponential form of the Euler product for a Dirichlet L-series turns \exp of that prime sum into the L-series \sum_n \chi(n)\, n^{-s}; and on \{\mathrm{Re}\, s > 1\} the analytically continued L-function agrees with its L-series. Composing the three gives \exp(A + B + T) = L(s, \chi). That \chi is nonprincipal (\chi \ne 1, witnessed at 3) is what makes the continued L entire. \blacksquare

⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [← tsum_neg_log_eq_layersA362583.tsum_neg_log_eq_layers {s : ℂ} (hs : 1 < s.re) :
  ∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s)) = layerA s + layerB s + layerT s**Per-`p` split summed over primes**: for `Re s > 1`,
`Σ_p -log(1 - χ(p) p^(-s)) = A(s) + B(s) + T(s)`.
Proof: rewrite each term with the per-prime split `neg_log_split`, then split the sum
by linearity of three absolutely convergent series (`Summable.tsum_add` twice) and
identify the `k = 2` piece as `layerB` (`tsum_term_two_eq_layerB`).
No double-sum rearrangement is involved.  hs1 < s.re, DirichletCharacter.LFunction_eq_LSeriesDirichletCharacter.LFunction_eq_LSeries {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
  DirichletCharacter.LFunction χ s = LSeries (fun x => χ ↑x) sFor `1 < re s` the L-function of a Dirichlet character agrees with the sum of the naive Dirichlet
series.
 χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  hs1 < s.re]
  exact`exact e` closes the main goal if its target type matches that of `e`.
 DirichletCharacter.LSeries_eulerProduct_exp_logDirichletCharacter.LSeries_eulerProduct_exp_log {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
  Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = LSeries (fun n => χ ↑n) sA variant of the Euler product for Dirichlet L-series.  χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  hs1 < s.re

Local dependency graph