EulerSine.integral_cos_mul_cos_pow_even
theorem EulerSine.integral_cos_mul_cos_pow_even :
∀ {z : ℂ} (n : ℕ),
z ≠ 0 →
(1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..Real.pi / 2, (2 * z * ↑x).cos * ↑x.cos ^ (2 * n + 2) =
(2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0 ..Real.pi / 2, (2 * z * ↑x).cos * ↑x.cos ^ (2 * n)
The theorem `EulerSine.integral_cos_mul_cos_pow_even` states that for any complex number `z` that is not zero, and any natural number `n`, the expression `(1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..Real.pi / 2, (2 * z * ↑x).cos * ↑x.cos ^ (2 * n + 2)` equals `(2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0 ..Real.pi / 2, (2 * z * ↑x).cos * ↑x.cos ^ (2 * n)`.
In more natural language, it means that, for a complex number `z` not equal to zero and a natural number `n`, the value of an integral involving the cosine of `(2 * z * x)` and the cosine of `x` raised to the power `(2 * n + 2)` multiplied by a fraction involving `z` and `n`, equals the value of a similar integral where the cosine of `x` is only raised to the power of `(2 * n)`, this being scaled by a fraction involving `n`.
In terms of LaTeX, the theorem states that for all $z \in \mathbb{C}$ (with $z \neq 0$) and $n \in \mathbb{N}$, the following equation holds:
$(1 - \frac{z^2}{(n+1)^2}) \int_0^{\frac{\pi}{2}} (2zx)\cos (x\cos^{2n+2}) = \frac{2n+1}{2n+2} \int_0^{\frac{\pi}{2}} (2zx)\cos (x\cos^{2n})$.
More concisely: For complex number $z \neq 0$ and natural number $n$, the integral of $(2zx)\cos(x\cos^{2n+2})$ from $0$ to $\frac{\pi}{2}$ equals $\frac{2n+1}{2n+2}$ times the integral of $(2zx)\cos(x\cos^{2n})$ from $0$ to $\frac{\pi}{2}$, with a constant term $(1-\frac{z^2}{(n+1)^2}$ multiplied to the former.
|
Complex.tendsto_euler_sin_prod
theorem Complex.tendsto_euler_sin_prod :
∀ (z : ℂ),
Filter.Tendsto (fun n => ↑Real.pi * z * (Finset.range n).prod fun j => 1 - z ^ 2 / (↑j + 1) ^ 2) Filter.atTop
(nhds (↑Real.pi * z).sin)
The Lean theorem `Complex.tendsto_euler_sin_prod` is representing Euler's infinite product formula for the complex sine function. This formula states that for any complex number `z`, the limit as `n` approaches infinity of the expression `πz` multiplied by the product over all natural numbers `j` less than `n` of `1 - z²/(j+1)²`, converges to the sine of `πz`. This is a fundamental result in complex analysis connecting the sine function to an infinite product.
More concisely: The limit of the product of `πz` and the sequence of terms `1 - z²/(j+1)²` as `j` approaches infinity, for any complex number `z`, equals the complex sine of `πz`.
|
Real.tendsto_euler_sin_prod
theorem Real.tendsto_euler_sin_prod :
∀ (x : ℝ),
Filter.Tendsto (fun n => Real.pi * x * (Finset.range n).prod fun j => 1 - x ^ 2 / (↑j + 1) ^ 2) Filter.atTop
(nhds (Real.pi * x).sin)
This theorem, often referred to as Euler's infinite product formula for the real sine function, states that for all real numbers `x`, the function defined as the product over a finite range `n` of terms of the form `1 - x^2 / (j + 1)^2`, preceded by the term `π*x`, tends to the sine of `π*x` as `n` tends to infinity. To put it more formally, given a real number `x`, the sequence defined by `π*x * ∏_{j=0}^{n} (1 - x^2 / (j+1)^2)` converges to `sin(π*x)` as `n` approaches infinity.
More concisely: For all real numbers `x`, the product `π×x×∏ₙ₁Ј⁺¹ (1 - x² / (j+1)²)` converges to `sin(π×x)` as `n` approaches infinity.
|
EulerSine.integral_cos_mul_cos_pow
theorem EulerSine.integral_cos_mul_cos_pow :
∀ {z : ℂ} {n : ℕ},
2 ≤ n →
z ≠ 0 →
(1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..Real.pi / 2, (2 * z * ↑x).cos * ↑x.cos ^ n =
(↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..Real.pi / 2, (2 * z * ↑x).cos * ↑x.cos ^ (n - 2)
This theorem, named "EulerSine.integral_cos_mul_cos_pow", states that for any complex number `z` which is not zero, and any natural number `n` that is equal to or greater than two, the equation
$$
(1 - 4z^2/n^2) * \int_{0}^{π/2} (2zx).cos * x.cos^n = (n - 1)/n * \int_{0}^{π/2} (2zx).cos * x.cos^{n - 2}
$$
holds true. It is important to note that this theorem also holds true when `z = 0`, but this particular case is not necessary for another theorem, `sin_pi_mul_eq`.
More concisely: For complex number `z` not equal to zero and natural number `n` greater than or equal to 2, the integral of `(2zx).cos * x.cos^n` from 0 to π/2 equals `(n - 1)/n * (1 - 4z^2/n^2) * ∫(0, π/2) (2zx).cos * x.cos^(n-2) dx`.
|
EulerSine.sin_pi_mul_eq
theorem EulerSine.sin_pi_mul_eq :
∀ (z : ℂ) (n : ℕ),
(↑Real.pi * z).sin =
((↑Real.pi * z * (Finset.range n).prod fun j => 1 - z ^ 2 / (↑j + 1) ^ 2) *
∫ (x : ℝ) in 0 ..Real.pi / 2, (2 * z * ↑x).cos * ↑x.cos ^ (2 * n)) /
↑(∫ (x : ℝ) in 0 ..Real.pi / 2, x.cos ^ (2 * n))
This theorem is a finite form of Euler's sine product formula. It states that for any complex number `z` and natural number `n`, the sine of `π*z` is equal to a certain expression involving the product over the range from 0 to `n`, an integral of a function involving `z` and `x` (the variable of integration) over the interval from 0 to `π/2`, and the reciprocal of another integral over the same interval. The product term depends on `z` and `n` and involves `z` squared divided by the square of `j+1` (with `j` denoting the element in the range), while the integrals involve power of cosine function and multiplication of cosine and `z`.
More concisely: For any complex number `z` and natural number `n`, the sine of `π*z` is equal to the product of `(z / √(j+1))` for `j` from `0` to `n-1`, multiplied by the integral from `0` to `π/2` of `cos(x)^n * z * cos(x) dx`, divided by the integral from `0` to `π/2` of `cos(x)^(n+1) dx`.
|
EulerSine.integral_cos_pow_eq
theorem EulerSine.integral_cos_pow_eq :
∀ (n : ℕ), ∫ (x : ℝ) in 0 ..Real.pi / 2, x.cos ^ n = 1 / 2 * ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ n
The theorem `EulerSine.integral_cos_pow_eq` states that for all natural numbers `n`, the integral of `cos^n(x)` from `0` to `π/2` is equal to half of the integral of `sin^n(x)` from `0` to `π`. This theorem connects the integrals of `cos^n(x)` and `sin^n(x)` over these specific intervals, a topic also explored in `Data.Real.Pi.Wallis` and in other places.
More concisely: The theorem asserts that for all natural numbers n, the integral of cos^n(x) from 0 to π/2 equals half the integral of sin^n(x) from 0 to π.
|