Real.hasSum_cosh
theorem Real.hasSum_cosh : ∀ (r : ℝ), HasSum (fun n => r ^ (2 * n) / ↑(2 * n).factorial) r.cosh
The theorem `Real.hasSum_cosh` states that for any real number `r`, the power series expansion of the hyperbolic cosine function `Real.cosh` has a sum. The series is given as the sum of the terms `r ^ (2 * n) / ↑(2 * n).factorial` for all non-negative integers `n`, where `r ^ (2 * n)` represents `r` raised to the power of `2 * n`, `↑(2 * n).factorial` represents the factorial of `2 * n` casted to a real number, and the division is real division. This theorem is essentially stating the Taylor series expansion of the hyperbolic cosine function, `Real.cosh`.
More concisely: The theorem `Real.hasSum_cosh` asserts that the power series representation of `Real.cosh(r)` as the sum of `r ^ (2 * n) / ↑(2 * n).factorial` for all non-negative integers `n` converges to `Real.cosh(r)`.
|
Complex.hasSum_cos'
theorem Complex.hasSum_cos' : ∀ (z : ℂ), HasSum (fun n => (z * Complex.I) ^ (2 * n) / ↑(2 * n).factorial) z.cos := by
sorry
This theorem, `Complex.hasSum_cos'`, states that for any complex number `z`, the series obtained by taking the nth term as `(z * Complex.I) ^ (2 * n) / ↑(Nat.factorial (2 * n))`, where `Complex.I` is the imaginary unit, `^` represents exponentiation, and `Nat.factorial` is the factorial function, converges to the complex cosine of `z`. In mathematical terms, this series is the power series expansion of the complex cosine function.
More concisely: The complex power series with terms `(z * Complex.I) ^ (2 * n) / Nat.factorial (2 * n)` converges to the complex cosine of `z`.
|
Complex.hasSum_cosh
theorem Complex.hasSum_cosh : ∀ (z : ℂ), HasSum (fun n => z ^ (2 * n) / ↑(2 * n).factorial) z.cosh
This theorem states that for all complex numbers `z`, the power series expansion of the hyperbolic cosine function, `Complex.cosh`, converges or 'has a sum'. The power series is given by the sum of the terms `z ^ (2 * n) / ↑(2 * n).factorial` for each nonnegative integer `n`, where `^` denotes exponentiation, `*` is multiplication, and `factorial` is the factorial function.
More concisely: The power series representation of the complex hyperbolic cosine function, given by the sum of `z ^ (2 * n) / (2 * n)!` for all nonnegative integers `n`, converges for all complex numbers `z`.
|
Real.hasSum_sin
theorem Real.hasSum_sin : ∀ (r : ℝ), HasSum (fun n => (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1).factorial) r.sin := by
sorry
The theorem `Real.hasSum_sin` states that for any real number `r`, the infinite sum (known as a power series) of the terms `(-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1).factorial`, where `n` ranges over all non-negative integers, is equal to the sine of `r`. This is essentially the Maclaurin series (a type of Taylor series centered at zero) expansion of the sine function.
More concisely: The Maclaurin series of the sine function equals the infinite sum of $(-1)^n \cdot r^{(2n+1)} / (2n+1)!$ for all real numbers $r$.
|
Real.hasSum_sinh
theorem Real.hasSum_sinh : ∀ (r : ℝ), HasSum (fun n => r ^ (2 * n + 1) / ↑(2 * n + 1).factorial) r.sinh
This theorem states that for any real number `r`, the power series expansion of the hyperbolic sine function `Real.sinh` is given by the infinite sum of terms where each term is `r` raised to the power `(2*n + 1)` divided by the factorial of `(2*n + 1)`, where `n` ranges over all non-negative integers. In mathematical terms, this is expressed as $\sinh(r) = \sum_{n=0}^{\infty} \frac{r^{2n+1}}{(2n+1)!}$. This theorem hence connects the hyperbolic sine function with the concept of a power series.
More concisely: The hyperbolic sine function can be represented as the infinite power series $\sum\_{n=0}^{\infty} \frac{r^{2n+1}}{(2n+1)!}$.
|
Real.hasSum_cos
theorem Real.hasSum_cos : ∀ (r : ℝ), HasSum (fun n => (-1) ^ n * r ^ (2 * n) / ↑(2 * n).factorial) r.cos
This theorem states that for any real number `r`, the power series `(-1) ^ n * r ^ (2 * n) / (2 * n).factorial` converges to the cosine of `r`. This series is the Taylor series expansion for the cosine function, where `n` ranges over all non-negative integers, `r` is the input, `(-1) ^ n` gives alternating signs, `r ^ (2 * n)` is the nth term in the power expansion, and `(2 * n).factorial` is the factorial of `2n`, which scales each term.
More concisely: For any real number `r`, the Taylor series of the cosine function, given by the sum of `(-1) ^ n * r ^ (2 * n) / (2 * n)!` for `n = 0, 1, 2, ...`, converges to `cos(r)`.
|
Complex.hasSum_sin'
theorem Complex.hasSum_sin' :
∀ (z : ℂ), HasSum (fun n => (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1).factorial / Complex.I) z.sin
The theorem `Complex.hasSum_sin'` states that for any complex number `z`, the infinite series made by taking successive odd powers of `z * Complex.I`, each divided by the factorial of its power and the imaginary unit `Complex.I`, converges to the complex sine of `z`. In mathematical terms, it's saying that the sum of `((z * Complex.I) ^ (2 * n + 1) / (Nat.factorial (2 * n + 1)) / Complex.I)` for all `n` from `0` to `∞` equals `Complex.sin z`. This is a restatement of the well-known power series representation for the sine function in terms of complex numbers.
More concisely: The theorem `Complex.hasSum_sin'` asserts that the infinite series of `((z * Complex.I) ^ (2 * n + 1) / (Nat.factorial (2 * n + 1)) / Complex.I)` for `n = 0, 1, 2, ...` converges to `Complex.sin z` for any complex number `z`.
|
Complex.hasSum_cos
theorem Complex.hasSum_cos : ∀ (z : ℂ), HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n).factorial) z.cos
This theorem states that for any complex number `z`, the power series expansion of `Complex.cos` converges and sums up to `z.cos`. The power series is defined as the sum of terms, where each term is `(-1) ^ n * z ^ (2 * n) / (2 * n).factorial` for each non-negative integer `n`. This sum is exactly the value of the cosine function at `z` in the complex numbers.
More concisely: The power series representation of Complex.cos(z) with terms (-1) ^ n * z ^ (2*n) / (2*n)! converges and equals to z.cos for any complex number z.
|
Complex.hasSum_sinh
theorem Complex.hasSum_sinh : ∀ (z : ℂ), HasSum (fun n => z ^ (2 * n + 1) / ↑(2 * n + 1).factorial) z.sinh
This theorem presents the power series expansion of the hyperbolic sine function for complex numbers. For any complex number `z`, the series is composed of terms `z ^ (2 * n + 1) / (2 * n + 1).factorial`, where `n` is a non-negative integer. The theorem states that the sum of this series equals to the hyperbolic sine of `z`.
More concisely: The hyperbolic sine function of a complex number `z` can be represented as the sum of the power series: `∑ (n : ℕ) (z ^ (2 * n + 1) / (2 * n + 1)! : ℝ)`, where `n` ranges over non-negative integers.
|
Complex.hasSum_sin
theorem Complex.hasSum_sin : ∀ (z : ℂ), HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1).factorial) z.sin
This theorem states that for any complex number `z`, the power series expansion of the sine function, `Complex.sin z`, converges and sums up to `z.sin`. The series is given by `(-1)^n * z^(2n + 1) / (2n + 1)!` where `n` ranges over all non-negative integers. This series, commonly referred to as the Taylor series expansion of the sine function, provides a mathematical representation for `Complex.sin z` in terms of an infinite sum of terms.
More concisely: For any complex number `z`, the power series $\sum\_{n=0}^\infty \frac{(-1)^n}{ (2n+1)! } (z)^{2n+1}$ converges and equals $z\cdot\sin(z)$.
|