isBigO_zero_zetaKernel₂
theorem isBigO_zero_zetaKernel₂ : zetaKernel₂ =O[nhdsWithin 0 (Set.Ioi 0)] fun t => (-Real.pi / t).exp / t.sqrt := by
sorry
This theorem provides a precise, yet not particularly convenient, mathematical bound for the function `zetaKernel₂` as `t` approaches `0` from positive values. Specifically, it states that `zetaKernel₂` is big O (denoted by `=O`) of the function `fun t => (-Real.pi / t).exp / t.sqrt` in the neighborhood of `0` that includes only positive real numbers (indicated by the neighborhood within `nhdsWithin 0 (Set.Ioi 0)`). This means that for small positive `t`, the value of `zetaKernel₂(t)` is bounded above by some multiple of `((-Real.pi / t).exp / t.sqrt)`. The function `fun t => (-Real.pi / t).exp / t.sqrt` is the exponential of the negative ratio of pi to `t`, divided by the square root of `t`.
More concisely: In the neighborhood of 0 that includes only positive real numbers, the function `zetaKernel₂` is big O of `(-Real.pi / t).exp / (t.sqrt)`.
|
continuousAt_zetaKernel₁
theorem continuousAt_zetaKernel₁ : ∀ {t : ℝ}, 0 < t → ContinuousAt zetaKernel₁ t
The theorem `continuousAt_zetaKernel₁` asserts that for any real number `t` that is greater than zero, the function `zetaKernel₁` is continuous at `t`. This function `zetaKernel₁` is defined as the sum over all natural numbers `n` of the expression `(-Real.pi * t * (n + 1) ^ 2).exp`, which is the exponential of the product of `-Real.pi`, `t`, and the square of `n+1`. The continuity of a function at a point, in the context of topological spaces, means that the output of the function tends to the value of the function at that point as the input approaches that point. In this case, as real numbers approach `t`, the value of `zetaKernel₁` at those numbers approaches the value of `zetaKernel₁` at `t`.
More concisely: For any real number `t` greater than zero, the function `zetaKernel₁` defined as the sum of `(-Real.pi * t * (n + 1) ^ 2).exp over all natural numbers `n` is continuous at `t`.
|
summable_exp_neg_pi_mul_nat_sq
theorem summable_exp_neg_pi_mul_nat_sq : ∀ {t : ℝ}, 0 < t → Summable fun n => (-Real.pi * t * (↑n + 1) ^ 2).exp := by
sorry
The theorem `summable_exp_neg_pi_mul_nat_sq` states that for every real number `t` greater than zero, the infinite sum defined by the function `n => (-Real.pi * t * (↑n + 1) ^ 2).exp` is summable. In other words, there exists a real number which is the limit of the partial sums of the sequence `(-π * t * (n + 1)²)`. This function represents an infinite series where each term is equal to the exponential of the negative product of π, `t`, and the square of `n + 1`, where `n` is a natural number.
More concisely: For every positive real number `t`, the infinite series sum of `(-π * t * (n + 1)²).exp`, where `n` ranges over natural numbers, is convergent.
|
locally_integrable_zetaKernel₁
theorem locally_integrable_zetaKernel₁ :
MeasureTheory.LocallyIntegrableOn zetaKernel₁ (Set.Ioi 0) MeasureTheory.volume
The theorem `locally_integrable_zetaKernel₁` states that the function `zetaKernel₁`, which is a series with each term being the complex exponential of the negative product of pi, a real number `t`, and the square of a natural number `n` increased by 1, is locally integrable on the open interval `(0, ∞)`. Local integrability in this context means that for every real number greater than 0, there is a neighborhood over which the `zetaKernel₁` function is Lebesgue integrable with respect to the Lebesgue measure.
More concisely: The function `zetaKernel₁` is locally integrable with respect to Lebesgue measure on the open interval (0, ∞).
|
locally_integrable_zetaKernel₂
theorem locally_integrable_zetaKernel₂ :
MeasureTheory.LocallyIntegrableOn zetaKernel₂ (Set.Ioi 0) MeasureTheory.volume
This theorem states that the function `zetaKernel₂`, which is the sum of the `zetaKernel₁` function and the function indicated on the interval from 0 to 1 (excluding 0, including 1) that maps a real number `t` to `(1 - 1 / t.sqrt) / 2`, is locally integrable on the set of all real numbers greater than zero. Here, local integrability is defined with respect to the Lebesgue measure, denoted by `MeasureTheory.volume`. In other words, for any real number greater than zero, one can find a neighborhood of this number where `zetaKernel₂` is integrable.
More concisely: The function `zetaKernel₂`, being the sum of `zetaKernel₁` and a function on (0,1] with the given expression, is locally integrable with respect to Lebesgue measure on the positive real numbers.
|
zeta_eq_tsum_one_div_nat_add_one_cpow
theorem zeta_eq_tsum_one_div_nat_add_one_cpow : ∀ {s : ℂ}, 1 < s.re → riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s := by
sorry
This theorem states that, for all complex numbers `s` such that the real part of `s` is greater than 1, the value of the Riemann zeta function at `s` equals the sum of the series 1 divided by `(n + 1) ^ s` for all natural numbers `n`. However, this equality holds only when the Dirichlet-series definition of the Riemann zeta function converges. This is not the case when the real part of `s` is less than or equal to 1, where the sum is divergent and a different definition is used to obtain the analytic continuation of the Riemann zeta function to all `s`.
More concisely: For complex numbers `s` with real part greater than 1, the Riemann zeta function equals the sum of the series 1 / (n + 1) ^ s for all natural numbers `n`, provided the Dirichlet series definition converges.
|
zeta_eq_tsum_one_div_nat_cpow
theorem zeta_eq_tsum_one_div_nat_cpow : ∀ {s : ℂ}, 1 < s.re → riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
The theorem `zeta_eq_tsum_one_div_nat_cpow` represents an alternate formulation of the Riemann Zeta function, denoted as `ζ(s)`. It states that for any complex number `s` with the real part greater than 1, the value of the Riemann Zeta function at `s` is equal to the infinite sum of the reciprocals of the `s`-th power of each natural number `n` (notated as `1 / ↑n ^ s`). This formulation does not require the addition of 1, as it relies on the fact that `0` raised to any non-zero `s` is defined to be `0`.
More concisely: For complex numbers `s` with real part greater than 1, the Riemann Zeta function `ζ(s)` equals the infinite sum of the reciprocal `1 / (↑n ^ s)` for each natural number `n`.
|
isBigO_atTop_zetaKernel₁
theorem isBigO_atTop_zetaKernel₁ : zetaKernel₁ =O[Filter.atTop] fun t => (-Real.pi * t).exp
This theorem states a bound for the function `zetaKernel₁` for large `t`. Specifically, it establishes that `zetaKernel₁` is a function that has Big O notation at the filter representing the limit towards infinity (`Filter.atTop`), equal to the function `fun t => Real.exp (-Real.pi * t)`. In other words, the growth rate of `zetaKernel₁` as `t` approaches infinity is at most the same as the growth rate of the function `fun t => Real.exp (-Real.pi * t)`. This implies that for large enough `t`, the absolute value of `zetaKernel₁(t)` is less than or equal to a constant multiple of `|Real.exp (-Real.pi * t)|`. The specific constant depends on `t`, but is independent of `zetaKernel₁` and the exponential function.
More concisely: The growth rate of `zetaKernel₁` as `t` approaches infinity is at most that of `Real.exp (-π*t)`.
|
differentiableAt_riemannZeta
theorem differentiableAt_riemannZeta : ∀ {s : ℂ}, s ≠ 1 → DifferentiableAt ℂ riemannZeta s
This theorem states that the Riemann zeta function is differentiable at any complex number `s` where `s` is not equal to 1. In other words, for any non-one complex number `s`, there exists a derivative of the Riemann zeta function at that point.
More concisely: The Riemann zeta function is complex differentiable for all complex numbers `s` except `s = 1`.
|
riemannZeta_neg_two_mul_nat_add_one
theorem riemannZeta_neg_two_mul_nat_add_one : ∀ (n : ℕ), riemannZeta (-2 * (↑n + 1)) = 0
This theorem states that the Riemann zeta function, denoted as ζ(s), has trivial zeroes at negative even integers, excluding zero itself. Specifically, for any natural number `n`, the value of the Riemann zeta function at `-2 * (n + 1)` (which are negative even integers) is zero. Trivial zeroes are a distinguished set of zeroes of the Riemann zeta function that are simple to calculate and understand.
More concisely: The Riemann zeta function has trivial zeroes at negative even integers, excluding zero.
|
differentiableAt_completed_zeta
theorem differentiableAt_completed_zeta : ∀ {s : ℂ}, s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ riemannCompletedZeta s := by
sorry
The theorem `differentiableAt_completed_zeta` asserts that the completed Riemann zeta function `Λ(s)`, defined as `Λ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s)` with minor corrections at `s = 0` and `s = 1`, is differentiable at every complex number `s` except `s = 0` and `s = 1`, where the function has simple poles. In other words, there exists a derivative for the completed Riemann zeta function at all points in the complex plane, excluding `s = 0` and `s = 1`.
More concisely: The completed Riemann zeta function `Λ(s)` is differentiable at every complex number `s ≠ 0, 1`.
|
riemannZeta_def
theorem riemannZeta_def :
riemannZeta = Function.update (fun s => ↑Real.pi ^ (s / 2) * riemannCompletedZeta s / (s / 2).Gamma) 0 (-1 / 2)
This theorem defines the Riemann zeta function, `riemannZeta`, in terms of the completed Riemann zeta function `riemannCompletedZeta` and the complex Gamma function `Complex.Gamma`. Specifically, for any complex number `s` other than `0`, `riemannZeta(s)` is equal to `π^(s/2) * riemannCompletedZeta(s) / Γ(s/2)`, where `Γ` denotes the complex Gamma function. However, at `s = 0`, `riemannZeta` is specifically defined to be `-1/2`.
More concisely: For complex numbers `s` other than 0, the Riemann zeta function `riemannZeta(s)` equals `π^(s/2) * riemannCompletedZeta(s) / Γ(s/2)`, while `riemannZeta(0)` is defined as `-1/2`.
|
hasMellin_one_div_sqrt_sub_one_div_two_Ioc
theorem hasMellin_one_div_sqrt_sub_one_div_two_Ioc :
∀ {s : ℂ},
1 / 2 < s.re →
HasMellin ((Set.Ioc 0 1).indicator fun t => (1 - 1 / ↑t.sqrt) / 2) s (1 / (2 * s) - 1 / (2 * s - 1))
The theorem `hasMellin_one_div_sqrt_sub_one_div_two_Ioc` states that for any complex number `s` with its real part greater than 1/2, the Mellin transform of the function defined over the interval (0, 1] (denoted by `Set.Ioc 0 1` in Lean, where `Ioc` stands for "Interval open-closed") that takes a real number `t` to `(1 - 1 / sqrt(t)) / 2`, is defined at `s` and evaluates to `1 / (2 * s) - 1 / (2 * s - 1)`. In other words, it calculates the Mellin transform of a function, often referred to as the "fudge factor" in the context of the `zetaKernel₂`, at a specific complex number `s` where the real part of `s` is greater than 1/2.
More concisely: For complex numbers `s` with real part greater than 1/2, the Mellin transform of the function `t ↔ (1 - 1 / sqrt(t)) / 2` over the interval (0, 1] equals `1 / (2 * s) - 1 / (2 * s - 1)`.
|
riemannCompletedZeta_residue_one
theorem riemannCompletedZeta_residue_one :
Filter.Tendsto (fun s => (s - 1) * riemannCompletedZeta s) (nhdsWithin 1 {1}ᶜ) (nhds 1)
The theorem `riemannCompletedZeta_residue_one` states that the residue of the completed Riemann zeta function `Λ(s)` at `s = 1` is equal to 1. More specifically, it asserts that the limit of the function `(s - 1) * Λ(s)` as `s` approaches 1, but does not equal 1 (the neighborhood around 1 excluding 1 itself), is 1. This means that an arbitrarily small neighborhood around 1, not including 1, when mapped through `(s - 1) * Λ(s)`, falls within a neighborhood of the value 1. This effectively describes the behavior of the completed Riemann zeta function near `s = 1`, providing a specific value (i.e., the residue) for the function at that point.
More concisely: The limit of $(s-1) \cdot \Lambda(s)$ as $s$ approaches 1 from the right is equal to 1.
|
differentiableAt_mellin_zetaKernel₁
theorem differentiableAt_mellin_zetaKernel₁ : ∀ {s : ℂ}, 1 / 2 < s.re → DifferentiableAt ℂ (mellin zetaKernel₁) s := by
sorry
The theorem `differentiableAt_mellin_zetaKernel₁` states that the Mellin transform of the first zeta kernel, which is a function defined as an infinite sum of complex exponentials, is differentiable at any complex number `s` where the real part of `s` is greater than `1/2`. In other words, the Mellin transform of the first zeta kernel admits a derivative at these points, implying the function is holomorphic in this region of the complex plane. This theorem is a cornerstone in complex analysis, particularly in the analysis of the Riemann zeta function and its Mellin transform.
More concisely: The Mellin transform of the first zeta kernel is differentiable at complex numbers with real part greater than 1/2.
|
differentiable_mellin_zetaKernel₂
theorem differentiable_mellin_zetaKernel₂ : Differentiable ℂ (mellin zetaKernel₂)
The theorem `differentiable_mellin_zetaKernel₂` states that the Mellin transform of the second zeta kernel is an entire function. This is expressed as "Differentiable ℂ (mellin zetaKernel₂)", where `ℂ` is the field of complex numbers, `mellin` is the Mellin transformation, and `zetaKernel₂` is the second zeta kernel. In mathematical terms, this is asserting that for every complex number, the derivative of the Mellin transform of the second zeta kernel at that point exists.
More concisely: The second zeta kernel's Mellin transform is an entire function.
|
zeta_nat_eq_tsum_of_gt_one
theorem zeta_nat_eq_tsum_of_gt_one : ∀ {k : ℕ}, 1 < k → riemannZeta ↑k = ∑' (n : ℕ), 1 / ↑n ^ k
This theorem, `zeta_nat_eq_tsum_of_gt_one`, states a special case of the Riemann zeta function's definition in terms of an infinite sum over the natural numbers. Specifically, when the argument of the zeta function is a natural number `k` greater than `1`, the zeta function `riemannZeta` evaluated at `k` is equal to the sum, for all natural numbers `n`, of `1 / n^k`. The term `n^k` here refers to `n` raised to the power of `k` using ordinary exponentiation (as opposed to complex power, or `cpow`).
More concisely: For natural numbers `k` greater than 1, the Riemann zeta function `riemannZeta k` equals the sum over all natural numbers `n` of `1 / n^k`.
|
riemannCompletedZeta₀_one_sub
theorem riemannCompletedZeta₀_one_sub : ∀ (s : ℂ), riemannCompletedZeta₀ (1 - s) = riemannCompletedZeta₀ s
This theorem states the functional equation for the completed Riemann zeta function, where the poles are removed, designated as `Λ₀`. Specifically, for any complex number `s`, the value of the function `Λ₀` at `1 - s` is equal to the value of the function at `s`. This is a cornerstone in the theory of the Riemann zeta function and has vital applications in number theory.
More concisely: The completed Riemann zeta function `Λ₀` satisfies the functional equation `Λ₀(1 - s) = Λ₀(s)`.
|
isBigO_zero_zetaKernel₁
theorem isBigO_zero_zetaKernel₁ : zetaKernel₁ =O[nhdsWithin 0 (Set.Ioi 0)] fun t => t ^ (-(1 / 2))
This theorem establishes a bound for the function `zetaKernel₁` as `t` approaches 0 from the right (i.e., `t` > 0). It states that `zetaKernel₁` is a Big O of the function `t ↦ t^-(1/2)` (meaning the function `t ↦ t^-(1/2)` serves as an upper bound for `zetaKernel₁`) within the neighborhood of 0 included in the open interval `(0, ∞)`. This neighborhood is represented with the `nhdsWithin` function, which denotes the intersection of a neighborhood of 0 and the interval `(0, ∞)`. The function `zetaKernel₁` is defined as the sum over all natural numbers `n` of the exponential of the product of `-πt` and the square of `n + 1`.
More concisely: The theorem asserts that the growth rate of `zetaKernel₁(t)` as `t` approaches 0 from the right is Big O of `t^(-1/2)`.
|
riemannCompletedZeta_one_sub
theorem riemannCompletedZeta_one_sub : ∀ (s : ℂ), riemannCompletedZeta (1 - s) = riemannCompletedZeta s
This theorem states the functional equation for the completed Riemann zeta function, denoted as `Λ`. It asserts that for any complex number `s`, the value of the completed Riemann zeta function at `(1 - s)` is equal to its value at `s`. In mathematical terms, this can be expressed as `Λ (1 - s) = Λ s` for all `s` in the complex numbers.
More concisely: The completed Riemann zeta function satisfies the functional equation `Λ(1 - s) = Λ(s)` for all complex numbers `s`.
|
differentiable_completed_zeta₀
theorem differentiable_completed_zeta₀ : Differentiable ℂ riemannCompletedZeta₀
The theorem `differentiable_completed_zeta₀` states that the modified completed Riemann zeta function, which is represented as `Λ(s) + 1 / s - 1 / (s - 1)`, is differentiable at any point in the complex plane. In other words, the theorem claims that this function is entire, meaning it has a derivative everywhere in the complex plane.
More concisely: The theorem `differentiable_completed_zeta₀` asserts that the modified completed Riemann zeta function `Λ(s) + 1 / s - 1 / (s - 1)` is an entire function in the complex plane.
|
riemannZeta_two_mul_nat
theorem riemannZeta_two_mul_nat :
∀ {k : ℕ},
k ≠ 0 →
riemannZeta (2 * ↑k) =
(-1) ^ (k + 1) * 2 ^ (2 * k - 1) * ↑Real.pi ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k).factorial
This theorem provides an explicit formula for the Riemann zeta function `ζ(s)` at even positive integers, specifically `ζ(2k)` for `k` as a non-zero natural number. The theorem states that `ζ(2k)` can be calculated as `(-1)^(k+1) * 2^(2k-1) * π^(2k) * Bernoulli(2k) / (2k)!`. The Bernoulli number used here is defined with a parity sign and `π` is defined as twice a zero of cosine in the interval [1, 2]. Note also equivalent formulations for other values at negative integers via the functional equation and for a version formulated explicitly as a sum.
More concisely: The Riemann zeta function `ζ(2k)` for a non-zero natural number `k` equals `(-1)^(k+1) * 2^(2k-1) * π^(2k) * Bernoulli(2k) / (2k)!`, where `π` is defined as twice a zero of cosine in the interval [1, 2] and `Bernoulli(2k)` denotes the Bernoulli number with the given parity sign.
|
zetaKernel₁_eq_jacobiTheta
theorem zetaKernel₁_eq_jacobiTheta : ∀ {t : ℝ}, 0 < t → zetaKernel₁ t = (jacobiTheta (↑t * Complex.I) - 1) / 2 := by
sorry
This theorem establishes a connection between the function `zetaKernel₁` and the Jacobi theta function on the upper half-plane. Specifically, for any real number `t` greater than zero, the value of `zetaKernel₁` at `t` is given by half of the value of the Jacobi theta function at the point `t` multiplied by the imaginary unit, minus 1. The theorem also explains that `zetaKernel₁` is defined as a sum over natural numbers (`ℕ`) instead of integers (`ℤ`) because this is more convenient for linking the zeta function to the Dirichlet series when the real part of the complex number is greater than 1.
More concisely: For any positive real number `t`, we have `zetaKernel₁ t = (1/2 * θ(t + ι) - 1)`, where `θ` is the Jacobi theta function and `ι` is the imaginary unit.
|
zetaKernel₂_one_div
theorem zetaKernel₂_one_div : ∀ {t : ℝ}, 0 ≤ t → zetaKernel₂ (1 / t) = ↑t.sqrt * zetaKernel₂ t
This theorem states the functional equation for the function `zetaKernel₂`. Specifically, for any real number `t` that is greater than or equal to zero, the value of `zetaKernel₂` at `1/t` is equal to the square root of `t` times the value of `zetaKernel₂` at `t`. This is a property of the modified zeta kernel `zetaKernel₂`, a complex-valued function defined on the real numbers, which, in addition to the zeta kernel `zetaKernel₁`, includes an indicator function that takes specific values in the interval (0,1).
More concisely: For any non-negative real number `t`, the modified zeta kernel `zetaKernel₂` satisfies `zetaKernel₂(1/t) = sqrt(t) * zetaKernel₂(t)`.
|
riemannZeta_residue_one
theorem riemannZeta_residue_one : Filter.Tendsto (fun s => (s - 1) * riemannZeta s) (nhdsWithin 1 {1}ᶜ) (nhds 1) := by
sorry
This theorem states that the residue of the Riemann zeta function `ζ(s)` at `s = 1` is equal to 1. More specifically, it says that the limit of the function `(s - 1) * ζ(s)` approaches 1 as `s` approaches 1 from any direction except directly from 1 (since `s` lies within the neighborhood of 1 but not including 1 itself). This is a fundamental result in complex analysis related to the properties of the Riemann zeta function.
More concisely: The limit of $(s-1) \cdot \zeta(s)$ as $s$ approaches 1 is equal to 1.
|
isBigO_zero_zetaKernel₂_rpow
theorem isBigO_zero_zetaKernel₂_rpow : ∀ (a : ℝ), zetaKernel₂ =O[nhdsWithin 0 (Set.Ioi 0)] fun t => t ^ a
This theorem, named `isBigO_zero_zetaKernel₂_rpow`, states that for any real number `a`, the function `zetaKernel₂` is big O at zero within the set of real numbers greater than zero with respect to the function `t` raised to the power of `a`. In mathematical terms, it means that as `t` approaches `0` from the positive side, the function `zetaKernel₂` grows at most as fast as the function `t^a`. The function `zetaKernel₂` is a modified zeta kernel, the sum of `zetaKernel₁` and a function defined on the open interval from `0` to `1`. This theorem provides a weaker but more usable bound for `zetaKernel₂` as `t` tends to `0`.
More concisely: For any real number `a`, the modified zeta kernel `zetaKernel₂` is big O at zero with respect to `t^a`.
|
isBigO_atTop_zetaKernel₂
theorem isBigO_atTop_zetaKernel₂ : zetaKernel₂ =O[Filter.atTop] fun t => (-Real.pi * t).exp
This theorem states that the function `zetaKernel₂` is bounded above for large `t` by the exponential of `-Real.pi * t`. Specifically, it states that as `t` approaches infinity (represented by `Filter.atTop`), the function `zetaKernel₂` is a member of the big O notation (`=O[Filter.atTop]`) of the function `fun t => (-Real.pi * t).exp`, which means there exists constants `C` and `t0` such that for all `t > t0`, `|zetaKernel₂(t)| ≤ C * |(-Real.pi * t).exp|`. Here, `zetaKernel₂` is a modified zeta kernel, which is composed of an initial zeta kernel plus an indicator function-defined adjustment for values of `t` in the interval `(0, 1]`. The exponential of `-Real.pi * t` is a rapidly decreasing function as `t` increases. The theorem is essential in estimating the size of `zetaKernel₂` for large `t`.
More concisely: As `t` approaches infinity, the absolute value of the modified zeta kernel `zetaKernel₂(t)` is bounded above by the exponential of `-π*t`.
|
riemannZeta_one_sub
theorem riemannZeta_one_sub :
∀ {s : ℂ},
(∀ (n : ℕ), s ≠ -↑n) →
s ≠ 1 →
riemannZeta (1 - s) =
2 ^ (1 - s) * ↑Real.pi ^ (-s) * s.Gamma * (↑Real.pi * (1 - s) / 2).sin * riemannZeta s
This is the Riemann zeta functional equation formulated for `ζ(s)`. The theorem states that for any complex number `s` which is not equal to 1 or the negative of any natural number `n`, the value of the Riemann zeta function at `1 - s` is equal to the product of `2` raised to the power of `1 - s`, π raised to the power of `-s`, the gamma function of `s`, the sine of `π(1 - s) / 2`, and the Riemann zeta function at `s`. In mathematical notation, it can be written as `ζ(1 - s) = 2^(1 - s) * π^(-s) * Γ(s) * sin(π(1 - s)/2) * ζ(s)`.
More concisely: For complex numbers `s` not equal to 1 or the negative of any natural number, `ζ(1 - s) = 2^(1 - s) * π^(-s) * Γ(s) * sin(π(1 - s)/2) * ζ(s)`.
|
integral_cpow_mul_exp_neg_pi_mul_sq
theorem integral_cpow_mul_exp_neg_pi_mul_sq :
∀ {s : ℂ},
0 < s.re →
∀ (n : ℕ),
∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (s - 1) * ↑(-Real.pi * t * (↑n + 1) ^ 2).exp =
↑Real.pi ^ (-s) * s.Gamma * (1 / (↑n + 1) ^ (2 * s))
The theorem `integral_cpow_mul_exp_neg_pi_mul_sq` states that for any complex number `s` with a positive real part, and for any natural number `n`, the integral over the set of real numbers greater than zero, of the function defined as `t` raised to the power (`s` - 1) times the exponential of (-π `t` (`n` + 1)²), is equal to π raised to the power -`s` times the Gamma function of `s` times 1 divided by (`n` + 1) raised to the power (2 * `s`).
In LaTeX terms, this theorem can be written as:
For any $s \in \mathbb{C}$ with $\Re(s) > 0$ and any $n \in \mathbb{N}$,
$$\int_{0}^{\infty} t^{s - 1} \cdot e^{-\pi t (n + 1)^2} dt = \frac{\pi^{-s} \cdot \Gamma(s)}{(n + 1)^{2s}}.$$
More concisely: For complex number $s$ with positive real part and natural number $n$, the integral of $t^{s-1}e^{-\pi(n+1)^2t}$ from 0 to infinity equals $\frac{\pi^{-s}\Gamma(s)}{(n+1)^{2s}}$.
|
riemannZeta_zero
theorem riemannZeta_zero : riemannZeta 0 = -1 / 2
This theorem asserts that the value of the Riemann zeta function, denoted as `ζ(s)`, at the input `0` is equal to `-1/2`. In mathematical terms, it is saying that ζ(0) = -1/2.
More concisely: The Riemann zeta function evaluates to `-1/2` at `s = 0`.
|