Part of: The mod-4 character, the k = 2 and k ≥ 3 layers of the Euler-product logarithm, the power series of the logarithm, and the divergence transfer.
DefinitionlayerB
The k = 2 layer B. Since \chi(p)^2 = 1 for odd p and \chi(2)^2 = 0,
B(s) \;=\; \tfrac12 \sum_{p \text{ odd}} p^{-2s},
realized in Lean with an if-mask at p = 2. It is holomorphic on
\Omega = \{\mathrm{Re}\, s > 1/2\} by locally uniform convergence of its partial sums.
Lean code for Definition layerB
-
⟲
def layerB (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 layerB (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`.
⟲:= (1ℂ / 2ℂ) * ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , if`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
(pNat.Primes : ℕ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.
) = 2ℕ then`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
0ℂ else`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
((pNat.Primes : ℕ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`. ) ^ (-(2ℂ * sℂ))