bernoulli_zero_fourier_coeff
theorem bernoulli_zero_fourier_coeff : ∀ {n : ℤ}, n ≠ 0 → bernoulliFourierCoeff 0 n = 0
This theorem states that for all integers `n` that are not equal to zero, the `n`-th Fourier coefficient of the `0`-th Bernoulli function on the interval `[0, 1]` is equal to `0`. In other words, except for the `0`-th Fourier coefficient, all other Fourier coefficients of the constant Bernoulli function `B₀(x) = 1` are `0`.
More concisely: For all non-zero integers `n`, the `n`-th Fourier coefficient of the constant Bernoulli function `B₀(x) = 1` on `[0, 1]` is equal to zero.
|
bernoulliFourierCoeff_zero
theorem bernoulliFourierCoeff_zero : ∀ {k : ℕ}, k ≠ 0 → bernoulliFourierCoeff k 0 = 0
This theorem states that the 0-th Fourier coefficient of the k-th Bernoulli function, denoted as `Bₖ(x)`, is equal to zero for all natural numbers `k` that are not equal to zero. The Bernoulli function is defined on the interval `[0, 1]`. The Fourier coefficient in this context represents the weight of the cosine and sine components in the Fourier series representation of the Bernoulli function.
More concisely: For all natural numbers `k`, the 0-th Fourier coefficient of `Bₖ(x)` is equal to zero if `k ≠ 0`.
|
bernoulliFourierCoeff_recurrence
theorem bernoulliFourierCoeff_recurrence :
∀ (k : ℕ) {n : ℤ},
n ≠ 0 →
bernoulliFourierCoeff k n =
1 / (-2 * ↑Real.pi * Complex.I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)
The theorem `bernoulliFourierCoeff_recurrence` states a recurrence relation in terms of the variable `k` for the `n`-th Fourier coefficient of the `k`-th Bernoulli function, denoted as `Bₖ`. For every natural number `k` and integer `n`, with the condition that `n` is not equal to zero, the `n`-th Fourier coefficient of `Bₖ` can be expressed as a fraction where the denominator is `-2πi` times `n` and the numerator is the difference of `1` (if `k` equals `1`) or `0` (otherwise) and the product of `k` and the `n`-th Fourier coefficient of the Bernoulli function of degree `k - 1`, `Bₖ₋₁`.
More concisely: For every natural number $k$ and integer $n$ with $n \neq 0$, the $n$-th Fourier coefficient of the $k$-th Bernoulli function $B\_k$ is given by $\dfrac{1 - (\text{if } k = 1 \text{ then } 1 \text{ else } 0) \cdot B\_{k-1}^{(n)}}{-2\pi i \cdot n}$, where $B\_{k-1}^{(n)}$ denotes the $n$-th Fourier coefficient of the Bernoulli function of degree $k-1$.
|
hasSum_L_function_mod_four_eval_three
theorem hasSum_L_function_mod_four_eval_three :
HasSum (fun n => 1 / ↑n ^ 3 * (Real.pi * ↑n / 2).sin) (Real.pi ^ 3 / 32)
This theorem provides an explicit formula for the sum of a specific series, namely `L(χ, 3)`, where `χ` is the unique nontrivial Dirichlet character modulo 4. This series is a sum of terms of the form `1 / n^3 * (πn / 2).sin` for every natural number `n`. The theorem asserts that this series converges and that its sum is `π^3 / 32`. In other words, this theorem is about the value of a special L-series at `s=3`, where the L-series is associated with the nontrivial Dirichlet character modulo 4.
More concisely: The L-series `L(χ, 3)` with the nontrivial Dirichlet character `χ` modulo 4 converges and equals `π^3 / 32`, where `L(χ, s)` is the sum of `1 / n^3 * (πn / 2).sin` for all natural numbers `n`.
|