Real.exp_zero
theorem Real.exp_zero : Real.exp 0 = 1
This theorem states that the value of the exponential function `Real.exp`, when evaluated at 0, is equal to 1. In mathematical terms, it's saying that $e^0 = 1$, where $e$ is the base of the natural logarithm.
More concisely: The base of the natural logarithm raised to the power of 0 equals 1. (equivalent to $e^0 = 1$)
|
Complex.exp_conj
theorem Complex.exp_conj : ∀ (x : ℂ), ((starRingEnd ℂ) x).exp = (starRingEnd ℂ) x.exp
The theorem `Complex.exp_conj` states that for all complex numbers `x`, the complex exponential function applied to the complex conjugate of `x` is equal to the complex conjugate of the complex exponential function applied to `x`. In other words, taking the complex conjugate commutes with the complex exponential function. It can be written in mathematical notation as follows: ∀ x ∈ ℂ, exp(x*) = (exp(x))* where 'exp' is the complex exponential function and '*' denotes the complex conjugate.
More concisely: For all complex numbers x, the complex conjugate of the complex exponential function equals the complex exponential function of the complex conjugate: exp(x\*). = (exp(x))\*.
|
Complex.abs_cos_add_sin_mul_I
theorem Complex.abs_cos_add_sin_mul_I : ∀ (x : ℝ), Complex.abs ((↑x).cos + (↑x).sin * Complex.I) = 1
The theorem `Complex.abs_cos_add_sin_mul_I` states that for every real number `x`, the absolute value of the complex number formed by the sum of the complex cosine of `x` and the complex sine of `x` multiplied by the imaginary unit `I`, is always equal to 1. This corresponds to the well-known result from trigonometry that the square root of the sum of the squares of the sine and cosine of any real number is 1, but extended to the complex number domain.
More concisely: The theorem asserts that |cos(x) + i*sin(x)| = 1 for all real numbers x.
|
Complex.sin_ofReal_im
theorem Complex.sin_ofReal_im : ∀ (x : ℝ), (↑x).sin.im = 0
This theorem states that the imaginary part of the complex sine of a real number is always zero. In other words, if `x` is any real number, and we compute the sine of `x` in the complex plane, the result is a complex number whose imaginary part is zero. In mathematical notation, this is essentially saying that $\Im(\sin(x)) = 0$ for all real numbers $x$.
More concisely: The imaginary part of the complex sine function is zero for all real numbers. In mathematical notation, $\Im(\sin(x)) = 0$ for all $x \in \mathbb{R}$.
|
Real.exp_lt_exp
theorem Real.exp_lt_exp : ∀ {x y : ℝ}, x.exp < y.exp ↔ x < y
This theorem states that for any two real numbers `x` and `y`, the exponential of `x` is less than the exponential of `y` if and only if `x` is less than `y`. In other words, the Real exponential function is strictly increasing. In mathematical terms, it says that for all $x, y \in \mathbb{R}$, $e^{x} < e^{y}$ if and only if $x < y$.
More concisely: The real exponential function is strictly increasing, that is, for all $x, y \in \mathbb{R}$, $x < y$ if and only if $e^x < e^y$.
|
Real.cosh_zero
theorem Real.cosh_zero : Real.cosh 0 = 1
This theorem states that the value of the real hyperbolic cosine function, `Real.cosh`, at the point zero is equal to one. In other words, in mathematical terms $\cosh(0) = 1$.
More concisely: The real hyperbolic cosine function evaluates to 1 at 0: `Real.cosh 0 = 1`.
|
Real.cos_neg
theorem Real.cos_neg : ∀ (x : ℝ), (-x).cos = x.cos
The theorem `Real.cos_neg` states that the cosine function has reflectional symmetry over the y-axis. Specifically, it asserts that for every real number `x`, the value of cosine at negative `x` (`Real.cos (-x)`) is equal to the value of cosine at `x` (`Real.cos x`). In mathematical terms, this is the property $\cos(-x) = \cos(x)$ for all real numbers `x`.
More concisely: The cosine function is reflectionally symmetric over the y-axis, that is, cos(-\x) = cos(\x) for all real numbers \x.
|
Complex.exp_ne_zero
theorem Complex.exp_ne_zero : ∀ (x : ℂ), x.exp ≠ 0
This theorem states that the complex exponential function is never zero for any complex number. In other words, for all complex numbers `x`, the result of applying the complex exponential function to `x` (`Complex.exp x`) is always non-zero.
More concisely: The complex exponential function, `Complex.exp`, never returns the zero value for any complex argument.
|
Complex.ofReal_exp
theorem Complex.ofReal_exp : ∀ (x : ℝ), ↑x.exp = (↑x).exp
This theorem states that for every real number `x`, the complex version of the real exponential of `x` is equal to the complex exponential of the complex version of `x`. In other words, when the real exponential function is applied to a real number and then raised to the complex plane, it equals applying the complex exponential function directly to the complex version of that real number. This theorem is verifying the behavior of the real exponential function when extended to the complex plane.
More concisely: For every real number x, the complex exponential of the complex number x equals the real exponential of x lifted to the complex plane.
|
Complex.cosh_add_sinh
theorem Complex.cosh_add_sinh : ∀ (x : ℂ), x.cosh + x.sinh = x.exp
This theorem states that for any complex number `x`, the sum of the complex hyperbolic cosine of `x` and the complex hyperbolic sine of `x` is equal to the complex exponential of `x`. In mathematical terms, this can be written as: ∀x ∈ ℂ, cosh(x) + sinh(x) = exp(x). This property is an important identity in complex analysis, analogous to the identity for real numbers where the sum of exponential of a number and its negative inverse is equal to the hyperbolic cosine of the number.
More concisely: For all complex numbers x, the sum of the complex hyperbolic cosine and sine functions of x is equal to the complex exponent function applied to x: cosh(x) + sinh(x) = exp(x).
|
Complex.cosh_sq_sub_sinh_sq
theorem Complex.cosh_sq_sub_sinh_sq : ∀ (x : ℂ), x.cosh ^ 2 - x.sinh ^ 2 = 1
This theorem states that for every complex number `x`, the square of the complex hyperbolic cosine of `x` minus the square of the complex hyperbolic sine of `x` is equal to 1. In mathematical terms, it signifies the identity $\cosh^2(x) - \sinh^2(x) = 1$ for all complex numbers `x`, where $\cosh(x)$ and $\sinh(x)$ are the complex hyperbolic cosine and sine of `x`, respectively. These are defined in terms of the complex exponential function: $\cosh(x) = \frac{e^x + e^{-x}}{2}$ and $\sinh(x) = \frac{e^x - e^{-x}}{2}$.
More concisely: For all complex numbers `x`, the relationship holds: $\frac{e^{2x} + 1}{2} - \frac{e^{2x} - 1}{2} = 1$, or equivalently, $\cosh^2(x) - \sinh^2(x) = 1$.
|
Complex.sin_two_mul
theorem Complex.sin_two_mul : ∀ (x : ℂ), (2 * x).sin = 2 * x.sin * x.cos
The theorem `Complex.sin_two_mul` states that for all complex numbers `x`, the sine of `2x` is equal to `2` times the sine of `x` times the cosine of `x`. This is the complex number version of the double-angle formula in trigonometry, which in mathematical notation is expressed as $\sin(2x) = 2 \sin(x) \cos(x)$.
More concisely: The complex sine function satisfies the double-angle identity: $\sin(2x) = 2\sin(x)\cos(x)$.
|
Complex.cosh_sub_sinh
theorem Complex.cosh_sub_sinh : ∀ (x : ℂ), x.cosh - x.sinh = (-x).exp
The theorem `Complex.cosh_sub_sinh` states that for any complex number `x`, the difference between the complex hyperbolic cosine of `x` and the complex hyperbolic sine of `x` equals the complex exponential function of the negative of `x`. In mathematical terms, this can be written as $\cosh(x) - \sinh(x) = e^{-x}$ for any complex number $x$. The complex hyperbolic cosine and sine functions are defined in terms of the complex exponential function, and this theorem represents a particular relationship between these functions.
More concisely: For any complex number $x$, $\cosh(x) - \sinh(x) = e^{-x}$.
|
Real.neg_one_le_sin
theorem Real.neg_one_le_sin : ∀ (x : ℝ), -1 ≤ x.sin
The theorem `Real.neg_one_le_sin` states that for all real numbers `x`, the sine of `x` is greater than or equal to -1. This is a property of the sine function, which always takes values between -1 and 1 for any input real number.
More concisely: For all real numbers x, -1 ≤ sin(x).
|
Real.exp_le_exp
theorem Real.exp_le_exp : ∀ {x y : ℝ}, x.exp ≤ y.exp ↔ x ≤ y
The theorem `Real.exp_le_exp` states that for all real numbers `x` and `y`, the exponential of `x` is less than or equal to the exponential of `y` if and only if `x` is less than or equal to `y`. This theorem formalizes the monotonicity of the exponential function over the real numbers in Lean 4. In other words, in the context of real numbers, the exponential function preserves the order of its inputs.
More concisely: For all real numbers x and y, x <= y implies exp x <= exp y.
|
Complex.exp_ofReal_im
theorem Complex.exp_ofReal_im : ∀ (x : ℝ), (↑x).exp.im = 0
This theorem states that for every real number `x`, the imaginary part of the exponential function of `x` interpreted as a complex number, denoted by `(Complex.exp ↑x).im`, is always equal to zero. In other words, the imaginary part of the complex exponential of a real number is always zero. This is equivalent to saying that the complex exponential of any real number lies on the real line in the complex plane.
More concisely: The imaginary part of the complex exponential function of a real number is equal to zero.
|
Complex.sinh_add
theorem Complex.sinh_add : ∀ (x y : ℂ), (x + y).sinh = x.sinh * y.cosh + x.cosh * y.sinh
The theorem `Complex.sinh_add` states that for all complex numbers `x` and `y`, the hyperbolic sine of the sum of `x` and `y` is equal to the product of the hyperbolic sine of `x` and the hyperbolic cosine of `y` added to the product of the hyperbolic cosine of `x` and the hyperbolic sine of `y`. In terms of mathematical notation, this can be written as:
For all $x, y \in \mathbb{C}$, $\sinh(x + y) = \sinh(x) \cdot \cosh(y) + \cosh(x) \cdot \sinh(y)$.
This is the addition formula for the complex hyperbolic sine function.
More concisely: The complex hyperbolic sine function satisfies the addition formula: $\sinh(x + y) = \sinh(x) \cosh(y) + \cosh(x) \sinh(y)$, for all $x, y \in \mathbb{C}$.
|
Real.exp_pos
theorem Real.exp_pos : ∀ (x : ℝ), 0 < x.exp
This theorem states that the real exponential function is always positive. In other words, for any real number `x`, the exponential of `x` (denoted as `exp(x)`) is strictly greater than zero. This is consistent with the mathematical property of the exponential function, which is always above the x-axis, never touching or crossing it.
More concisely: For all real numbers x, exp(x) > 0.
|
Complex.ofReal_exp_ofReal_re
theorem Complex.ofReal_exp_ofReal_re : ∀ (x : ℝ), ↑(↑x).exp.re = (↑x).exp
This theorem states that for any real number 'x', the real part of the complex exponential of 'x' (when 'x' is considered as a complex number by treating it as the real part and setting the imaginary part to zero), is equal to the complex exponential of 'x' itself. This identifies a property of the complex exponential function - when applied to real numbers, it essentially behaves like the real exponential function with respect to the real part.
More concisely: The real part of the complex exponential of a real number 'x' is equal to the complex exponential of 'x' itself. In other words, Re(e^(x + i*0)) = e^x.
|
Real.abs_cos_le_one
theorem Real.abs_cos_le_one : ∀ (x : ℝ), |x.cos| ≤ 1
This theorem states that for all real numbers `x`, the absolute value of the cosine of `x` is less than or equal to 1. In mathematical terms, this can be written as: ∀ (x : ℝ), |cos(x)| ≤ 1. This is a foundational result in trigonometry that sets the range of the cosine function, ensuring that it never exceeds the limits of the unit circle, i.e., -1 to 1.
More concisely: For all real numbers x, the absolute value of cos(x) is bounded by 1, that is, |cos(x)| ≤ 1.
|
Real.exp_ne_zero
theorem Real.exp_ne_zero : ∀ (x : ℝ), x.exp ≠ 0
This theorem states that the real exponential function is never zero. In other words, for all real numbers `x`, the value of the exponential function at `x`, denoted by `Real.exp x`, is not equal to zero. This is a well-known property of the exponential function in mathematics, which can be expressed as $\forall x \in \mathbb{R}, \exp(x) \neq 0$.
More concisely: For all real numbers x, the exponential function Real.exp x is never zero. Equivalently, ∀x:ℝ, Real.exp x ≠ 0.
|
Complex.cosh_mul_I
theorem Complex.cosh_mul_I : ∀ (x : ℂ), (x * Complex.I).cosh = x.cos
This theorem states that for every complex number `x`, the complex hyperbolic cosine of the product of `x` and the imaginary unit equals the complex cosine of `x`. In mathematical terms, it says that `cosh(ix) = cos(x)` for all `x` in the complex numbers, where `cosh` is the complex hyperbolic cosine function defined via the exponential function, `cos` is the complex cosine function also defined via the exponential function, and `i` is the imaginary unit.
More concisely: The complex hyperbolic cosine of the product of a complex number `x` and the imaginary unit `i` equals the complex cosine of `x`, that is, `cosh(ix) = cos(x)` for all `x` in the complex numbers.
|
Complex.sin_mul_I
theorem Complex.sin_mul_I : ∀ (x : ℂ), (x * Complex.I).sin = x.sinh * Complex.I
This theorem states that for every complex number `x`, the sine of `x` multiplied by the imaginary unit `I` is equal to the hyperbolic sine of `x` multiplied by the imaginary unit `I`. In other words, it is showing the relationship between the complex sine function and the complex hyperbolic sine function when their inputs are multiplied by the imaginary unit. This can also be expressed mathematically as `sin(xI) = sinh(x)I` for all complex `x`.
More concisely: The theorem asserts that for all complex numbers x, sin(x \* i) = sinh(x) \* i, where i is the imaginary unit.
|
Complex.cos_add_sin_mul_I_pow
theorem Complex.cos_add_sin_mul_I_pow :
∀ (n : ℕ) (z : ℂ), (z.cos + z.sin * Complex.I) ^ n = (↑n * z).cos + (↑n * z).sin * Complex.I
De Moivre's formula in complex arithmetic states that for any natural number 'n' and any complex number 'z', the 'n'-th power of the sum of the cosine of 'z' and the product of the sine of 'z' and the imaginary unit is equal to the sum of the cosine of the product of 'n' and 'z' and the product of the sine of that same product and the imaginary unit. This theorem is a fundamental result in complex analysis and provides a deep connection between trigonometry and complex exponentiation.
More concisely: For any natural number n and complex number z, (cos(z) + i*sin(z))^n equals cos(n*z) + i*sin(n*z).
|
Complex.two_sinh
theorem Complex.two_sinh : ∀ (x : ℂ), 2 * x.sinh = x.exp - (-x).exp
This theorem states that for any complex number `x`, the value of `2` times the complex hyperbolic sine of `x` is equal to the difference between the complex exponential of `x` and the complex exponential of `-x`. Here, the complex hyperbolic sine and complex exponential functions are defined in terms of their corresponding Taylor series.
More concisely: The theorem asserts that for any complex number `x`, the equality `2⁝sh(x) = exp(x) - exp(-x)` holds, where `sh` denotes the complex hyperbolic sine and `exp` the complex exponential, both defined using their respective Taylor series.
|
Complex.cos_neg
theorem Complex.cos_neg : ∀ (x : ℂ), (-x).cos = x.cos
This theorem states that the complex cosine function is an even function. In other words, for any complex number `x`, the cosine of the negation of `x` (`-x`) is equal to the cosine of `x` itself. This mirrors the property of the real-valued cosine function. In mathematical notation, this would be represented as: ∀x ∈ ℂ, cos(-x) = cos(x).
More concisely: The complex cosine function is an even function, that is, cos(-x) = cos(x) for all x in ℂ.
|
Complex.exp_zero
theorem Complex.exp_zero : Complex.exp 0 = 1
The theorem `Complex.exp_zero` states that the value of the complex exponential function at zero is equal to one. In other words, it asserts that `exp(0) = 1` in the field of complex numbers, which echoes the familiar rule from real-number calculus.
More concisely: The complex exponential function evaluates to 1 at 0. (exp(0) = 1 in the complex numbers)
|
Complex.exp_nat_mul
theorem Complex.exp_nat_mul : ∀ (x : ℂ) (n : ℕ), (↑n * x).exp = x.exp ^ n
The theorem `Complex.exp_nat_mul` states that for any complex number `x` and any natural number `n`, the exponential of the product of `n` and `x` is equal to the exponential of `x` raised to the power `n`. In mathematical notation, this is equivalent to saying that for all `x` in the set of complex numbers and `n` in the set of natural numbers, \(e^{nx} = (e^x)^n\).
More concisely: For all complex numbers x and natural numbers n, $e^{nx} = (e^x)^n$.
|
Mathlib.Data.Complex.Exponential._auxLemma.8
theorem Mathlib.Data.Complex.Exponential._auxLemma.8 : ∀ (x : ℝ), (↑x).cos = ↑x.cos
This theorem states that for any real number `x`, the complex cosine of `x` (when `x` is treated as a complex number with imaginary part 0) is equal to the real cosine of `x` treated as a real number. Here, the complex cosine is defined via the exponential function, and the real cosine is defined as the real part of the complex cosine. In mathematical terms, for any real number `x`, `Complex.cos (x)` is equal to `Real.cos (x)`.
More concisely: For any real number x, the complex cosine of x treated as a complex number with imaginary part 0 equals the real part of the complex cosine of x, which is equivalent to the real cosine of x. In other words, `Real.cos x = Re part (Complex.cos x)`.
|
Complex.tan_eq_sin_div_cos
theorem Complex.tan_eq_sin_div_cos : ∀ (x : ℂ), x.tan = x.sin / x.cos
This theorem states that for every complex number `x`, the complex tangent of `x`, denoted by `Complex.tan x`, is equal to the quotient of the complex sine of `x` and the complex cosine of `x`. Here, `Complex.sin x` and `Complex.cos x` are defined in terms of the complex exponential function. The complex sine of a number `z` is defined as `(Complex.exp (-z * Complex.I) - Complex.exp (z * Complex.I)) * Complex.I / 2` and the complex cosine of a number `z` is defined as `(Complex.exp (z * Complex.I) + Complex.exp (-z * Complex.I)) / 2`.
More concisely: The complex tangent of a complex number `x` is equal to the quotient of its complex sine and complex cosine, where complex sine is defined as the imaginary part of the exponential function `Complex.exp (x * Complex.I) - Complex.exp (-x * Complex.I)` divided by 2, and complex cosine is defined as the real part of the exponential function `Complex.exp (x * Complex.I) + Complex.exp (-x * Complex.I)` divided by 2.
|
Complex.exp_mul_I
theorem Complex.exp_mul_I : ∀ (x : ℂ), (x * Complex.I).exp = x.cos + x.sin * Complex.I
The theorem `Complex.exp_mul_I` states that for all complex numbers `x`, the exponential of `x` multiplied by the imaginary unit equals the complex cosine of `x` plus the complex sine of `x` multiplied by the imaginary unit. In mathematical terms, it expresses the well-known Euler's formula in complex analysis: e^(ix) = cos(x) + i sin(x) for any complex number x.
More concisely: For all complex numbers x, Complex.exp x = Complex.cos x + Complex.i * Complex.sin x.
|
Complex.sinh_conj
theorem Complex.sinh_conj : ∀ (x : ℂ), ((starRingEnd ℂ) x).sinh = (starRingEnd ℂ) x.sinh
The theorem `Complex.sinh_conj` states that for every complex number `x`, the complex hyperbolic sine of the complex conjugate of `x` is equal to the complex conjugate of the complex hyperbolic sine of `x`. In other words, the complex hyperbolic sine function commutes with complex conjugation. This can be represented in mathematical notation as follows: for all `x` in ℂ, sinh(conj(x)) = conj(sinh(x)), where "conj" denotes the complex conjugate operation, and "sinh" denotes the complex hyperbolic sine function.
More concisely: For all complex numbers x, the complex conjugate of the hyperbolic sine of x is equal to the hyperbolic sine of the complex conjugate of x. In other words, sinh(conj(x)) = conj(sinh(x)) in the complex numbers.
|
Complex.exp_eq_exp_re_mul_sin_add_cos
theorem Complex.exp_eq_exp_re_mul_sin_add_cos :
∀ (x : ℂ), x.exp = (↑x.re).exp * ((↑x.im).cos + (↑x.im).sin * Complex.I)
This theorem states that for any complex number `x`, the exponential of `x` is equal to the product of the exponential of the real part of `x` and the sum of the cosine of the imaginary part of `x` and the product of the sine of the imaginary part of `x` and the imaginary unit `I`. In mathematical terms, it expresses the identity: $e^{x} = e^{Re(x)} * (cos(Im(x)) + sin(Im(x)) * i)$ for all complex numbers $x$. Here, $Re(x)$ and $Im(x)$ respectively denote the real and imaginary parts of the complex number $x$, and $i$ is the imaginary unit.
More concisely: For any complex number x, the exponential function equals the product of the exponential of its real part and the cosine of its imaginary part plus the sine of its imaginary part times the imaginary unit i: $e^x = e^{Re(x)} \cdot (\cos(Im(x)) + \sin(Im(x)) \cdot i)$.
|
Real.cosh_eq
theorem Real.cosh_eq : ∀ (x : ℝ), x.cosh = (x.exp + (-x).exp) / 2
This theorem expresses the definition of the hyperbolic cosine function, `cosh`, for any real number `x`. It states that the hyperbolic cosine of `x` is equal to the average of the exponential function of `x` and the exponential function of `-x`, i.e., `(exp(x) + exp(-x)) / 2`.
More concisely: The hyperbolic cosine function, `cosh(x)`, is defined as the average of `exp(x)` and `exp(-x)`, i.e., `(exp(x) + exp(-x)) / 2`.
|
Real.exp_monotone
theorem Real.exp_monotone : Monotone Real.exp
The theorem `Real.exp_monotone` states that the real exponential function, denoted by `Real.exp`, is monotone. In other words, given two real numbers where the first is less than or equal to the second, the exponential of the first number will also be less than or equal to the exponential of the second number.
More concisely: For all real numbers x and y with x ≤ y, it holds that Real.exp x ≤ Real.exp y.
|
Real.tan_neg
theorem Real.tan_neg : ∀ (x : ℝ), (-x).tan = -x.tan
This theorem states that the real tangent function has odd symmetry. Specifically, for any real number `x`, the tangent of its negative, `tan(-x)`, is equal to the negative of the tangent of `x`, `-tan(x)`.
More concisely: The real tangent function is an odd function, i.e., tan(-x) = -tan(x) for all real numbers x.
|
Complex.ofReal_tan
theorem Complex.ofReal_tan : ∀ (x : ℝ), ↑x.tan = (↑x).tan
This theorem states that for any real number `x`, the complex number equivalent of the real tangent function of `x` is equal to the complex tangent function of `x` as a complex number. In mathematical terms, this can be expressed as: for all real numbers `x`, `Complex.tan (x)` equals `Real.tan (x)`, where `Complex.tan` and `Real.tan` are the tangent functions extended to the complex and real numbers, respectively.
More concisely: For all real numbers x, the complex tangent of x equals the real tangent of x. (Complex.tan x = Real.tan x)
|
Complex.sinh_mul_I
theorem Complex.sinh_mul_I : ∀ (x : ℂ), (x * Complex.I).sinh = x.sin * Complex.I
The theorem `Complex.sinh_mul_I` states that for any complex number `x`, the complex hyperbolic sine of `x` times the imaginary unit (`Complex.I`) is equal to the complex sine of `x` times the imaginary unit (`Complex.I`). In terms of mathematical notation, this can be written as: for all complex numbers x, `sinh(x * i) = sin(x) * i`. This theorem links the complex hyperbolic sine function and the complex sine function under multiplication by the imaginary unit.
More concisely: For all complex numbers x, sinh(x * I) = sin(x) * I.
|
Complex.exp_add
theorem Complex.exp_add : ∀ (x y : ℂ), (x + y).exp = x.exp * y.exp
This theorem states that for any two complex numbers `x` and `y`, the exponential of the sum `x + y` is equal to the product of the exponential of `x` and the exponential of `y`. In mathematical terms, this corresponds to the well-known property of the exponential function, written as `exp(x + y) = exp(x) * exp(y)`, but extended to the realm of complex numbers.
More concisely: For all complex numbers x and y, exp(x + y) = exp(x) * exp(y).
|
Complex.sin_sq_add_cos_sq
theorem Complex.sin_sq_add_cos_sq : ∀ (x : ℂ), x.sin ^ 2 + x.cos ^ 2 = 1
This theorem states that for any complex number `x`, the square of the complex sine of `x` plus the square of the complex cosine of `x` equals 1. This is a complex analog of the well-known trigonometric identity $\sin^2 \theta + \cos^2 \theta = 1$. Here, `Complex.sin x` and `Complex.cos x` represent the complex sine and complex cosine of `x`, respectively, both of which are defined in terms of the complex exponential function.
More concisely: For any complex number x, the sum of the squares of its complex sine and complex cosine equals 1: |Complex.sin x|² + |Complex.cos x|² = 1.
|
Real.exp_le_exp_of_le
theorem Real.exp_le_exp_of_le : ∀ {x y : ℝ}, x ≤ y → x.exp ≤ y.exp
This theorem states that for all real numbers `x` and `y`, if `x` is less than or equal to `y`, then the exponential of `x` is less than or equal to the exponential of `y`. The exponential function here is the real exponential function, which is defined as the real part of the complex exponential. In mathematical terms, it can be written as: for all $x, y \in \mathbb{R}$, if $x \leq y$ then $\exp(x) \leq \exp(y)$. This is a property of the exponential function ensuring that it is a monotonically increasing function in the real numbers.
More concisely: For all real numbers x and y, if x <= y then exp(x) <= exp(y).
|
Real.cosh_neg
theorem Real.cosh_neg : ∀ (x : ℝ), (-x).cosh = x.cosh
This theorem states that the real hyperbolic cosine function has the property of evenness. In other words, for any real number `x`, the value of the hyperbolic cosine function at `-x` is the same as its value at `x`. This mirrors the mathematical statement that $\cosh(-x) = \cosh(x)$ for all real numbers `x`.
More concisely: The hyperbolic cosine function is an even function, i.e., $\cosh(-x) = \cosh(x)$ for all real numbers $x$.
|
Mathlib.Data.Complex.Exponential._auxLemma.9
theorem Mathlib.Data.Complex.Exponential._auxLemma.9 : ∀ (x : ℝ), (↑x).tan = ↑x.tan
The theorem `Mathlib.Data.Complex.Exponential._auxLemma.9` states that for all real numbers `x`, the complex tangent of `x` is equal to the real part of the tangent of `x`. This is essentially stating that the complex tangent function, when applied to a real number (which is treated as a complex number with zero imaginary part), results in a complex number which has its real part equal to the standard tangent function applied to the same real number.
More concisely: The theorem asserts that the real part of the complex tangent function equals the standard real tangent function for all real numbers.
|
Real.exp_strictMono
theorem Real.exp_strictMono : StrictMono Real.exp
The theorem `Real.exp_strictMono` states that the real exponential function, denoted as `Real.exp`, is strictly monotone. In other words, for any two real numbers `a` and `b`, if `a` is less than `b` then the exponential of `a` (i.e., `Real.exp a`) is less than the exponential of `b` (i.e., `Real.exp b`). This property is a fundamental characteristic of the exponential function in real numbers.
More concisely: The real exponential function `Real.exp` is strictly increasing.
|
Real.sinh_neg
theorem Real.sinh_neg : ∀ (x : ℝ), (-x).sinh = -x.sinh
This theorem states that the real hyperbolic sine function has the property of oddness. Specifically, for any real number `x`, the hyperbolic sine of the negative of `x` is equal to the negative of the hyperbolic sine of `x`. In mathematical notation, this can be written as $\sinh(-x) = -\sinh(x)$ for all $x \in \mathbb{R}$.
More concisely: The hyperbolic sine function is an odd function, i.e., $\sinh(-x) = -\sinh(x)$ for all $x \in \mathbb{R}$.
|
Complex.abs_exp
theorem Complex.abs_exp : ∀ (z : ℂ), Complex.abs z.exp = z.re.exp
This theorem states that for every complex number `z`, the absolute value of the exponential of `z` is equal to the real exponential of the real part of `z`. In other words, if we calculate the exponential function of a complex number and then take its absolute value, the result is the same as if we had taken the real part of the complex number and computed the real exponential of that. This is formulated mathematically as `|e^z| = e^Re(z)` for all complex numbers `z`.
More concisely: The absolute value of the complex exponential function equals the real exponential of the real part for all complex numbers: |e^z| = e^(Re(z)).
|
Real.exp_injective
theorem Real.exp_injective : Function.Injective Real.exp
The theorem `Real.exp_injective` states that the real exponential function, denoted as `Real.exp`, is injective. In other words, given any two real numbers `x` and `y`, if the exponential of `x` is equal to the exponential of `y` (i.e., `Real.exp x = Real.exp y`), then `x` must be equal to `y`. This property is fundamental to the exponential function in real-number calculus.
More concisely: The real exponential function `Real.exp` is injective, that is, for all real numbers `x` and `y`, if `Real.exp x = Real.exp y`, then `x = y`.
|
Real.sin_sq
theorem Real.sin_sq : ∀ (x : ℝ), x.sin ^ 2 = 1 - x.cos ^ 2
This theorem states that for all real numbers `x`, the square of the sine of `x` is equal to 1 subtracted by the square of the cosine of `x`. In mathematical terms, it's expressing the well-known trigonometric identity $\sin^2(x) = 1 - \cos^2(x)$ for all real `x`. This identity is a consequence of the Pythagorean identity in trigonometry.
More concisely: For all real numbers x, the square of sine(x) equals one minus the square of cosine(x). In mathematical notation: ∀x:ℝ, sin²(x) = 1 - cos²(x).
|
Real.add_one_le_exp
theorem Real.add_one_le_exp : ∀ (x : ℝ), x + 1 ≤ x.exp
This theorem states that for all real numbers `x`, the sum of `x` and one is less than or equal to the exponential of `x`. In mathematical terms, it is saying that for all `x` in ℝ, `x + 1 ≤ exp(x)`.
More concisely: For all real numbers x, the exponential function exp(x) is greater than or equal to the sum of x and 1: x + 1 ≤ exp(x). (Note: The original statement was incorrect, so I corrected it to reflect the actual theorem.)
|
Complex.ofReal_cos_ofReal_re
theorem Complex.ofReal_cos_ofReal_re : ∀ (x : ℝ), ↑(↑x).cos.re = (↑x).cos
This theorem states that for every real number `x`, the real part of the complex cosine of `x` (when `x` is considered as a complex number) is equal to the complex cosine of `x`. In other words, taking the real part doesn't change the value of the complex cosine function when it's applied to a real number. More formally, for all real numbers `x`, we have `ℝ(Complex.cos(ℂx)) = Complex.cos(ℂx)`.
More concisely: The real part of the complex cosine of a real number equals the complex cosine of that real number. In Lean notation, for all real numbers x, ℝ(Complex.cos(ℂx)) = Complex.cos(ℂx).
|
Real.sin_zero
theorem Real.sin_zero : Real.sin 0 = 0
This theorem states that the sine of zero in real numbers is zero. In other words, applying the real sine function `Real.sin` to the argument `0` results in `0`. This is consistent with the standard mathematical understanding of the sine function, i.e., $\sin(0) = 0$.
More concisely: The real sine function evaluates to zero at zero: `Real.sin 0 = 0`.
|
Real.sin_neg
theorem Real.sin_neg : ∀ (x : ℝ), (-x).sin = -x.sin
The theorem `Real.sin_neg` states that the sine function in real numbers, `Real.sin`, is an odd function. That is, for any real number `x`, the sine of the negative of `x` (i.e., `-x`) is equal to the negative of the sine of `x` (i.e., `-Real.sin x`). This is a common property of the sine function in mathematics and is often written as: sin(-x) = -sin(x).
More concisely: The sine function is an odd function, i.e., sin(-x) = -sin(x) for all real numbers x.
|
Real.tan_zero
theorem Real.tan_zero : Real.tan 0 = 0
This theorem states that the real tangent function, when evaluated at zero, is equal to zero. In mathematical terms, it can be written as $\tan(0) = 0$. It expresses a well-known property of the tangent function from trigonometry in the context of real numbers.
More concisely: The real tangent function equals zero at zero: $\tan(0) = 0$.
|
Complex.exp_neg
theorem Complex.exp_neg : ∀ (x : ℂ), (-x).exp = x.exp⁻¹
This theorem states that for all complex numbers `x`, the complex exponential of the negation of `x` is equal to the multiplicative inverse of the complex exponential of `x`. In other words, `Complex.exp (-x) = 1/(Complex.exp x)`. This mirrors the familiar property from real numbers that the exponential function of a negative input is the reciprocal of the exponential function with the same but positive input.
More concisely: The complex exponential function is its own multiplicative inverse for the negated argument: `Complex.exp (-x) = 1 / (Complex.exp x)`.
|
Complex.cos_two_mul
theorem Complex.cos_two_mul : ∀ (x : ℂ), (2 * x).cos = 2 * x.cos ^ 2 - 1
This theorem states that for every complex number `x`, the cosine of twice this number, computed using the complex cosine function, is equal to twice the square of the cosine of the original number minus one. In mathematical terms, for all complex numbers x, we have cos(2x) = 2cos²(x) - 1, where cos is the complex cosine function defined in terms of the complex exponential function.
More concisely: For all complex numbers x, cos(2x) = 2 cos²(x) - 1.
|
Complex.cos_add
theorem Complex.cos_add : ∀ (x y : ℂ), (x + y).cos = x.cos * y.cos - x.sin * y.sin
This theorem, `Complex.cos_add`, states that for any two complex numbers `x` and `y`, the cosine of the sum of `x` and `y` is equal to the product of the cosine of `x` and the cosine of `y` minus the product of the sine of `x` and the sine of `y`. This is the complex version of the standard trigonometric identity for the cosine of a sum, $\cos(x+y) = \cos(x)\cos(y) - \sin(x)\sin(y)$.
More concisely: The cosine of the sum of two complex numbers is equal to the product of their cosines minus the product of their sines.
|
Real.add_one_lt_exp
theorem Real.add_one_lt_exp : ∀ {x : ℝ}, x ≠ 0 → x + 1 < x.exp
The theorem `Real.add_one_lt_exp` asserts that for all real numbers `x`, provided `x` is not equal to zero, `x + 1` is strictly less than the exponential of `x`, denoted as `Real.exp x`. In other words, for each non-zero real number, when you increment it by 1, the result is always smaller than the exponential of the original number.
More concisely: For all non-zero real numbers x, x + 1 < Real.exp x.
|
Complex.cos_mul_I
theorem Complex.cos_mul_I : ∀ (x : ℂ), (x * Complex.I).cos = x.cosh
This theorem states that for all complex numbers `x`, the complex cosine of `x` multiplied by the imaginary unit is equal to the complex hyperbolic cosine of `x`. In other words, `Complex.cos (x * Complex.I) = Complex.cosh x` for all `x` in the complex numbers. This relationship connects the trigonometric and hyperbolic functions in the context of complex numbers.
More concisely: The complex function ` Complex.cos(x * Complex.I)` equals `Complex.cosh x` for all complex numbers `x`.
|
Complex.ofReal_sinh
theorem Complex.ofReal_sinh : ∀ (x : ℝ), ↑x.sinh = (↑x).sinh
This theorem states that for every real number `x`, the complex number equivalent of the real hyperbolic sine of `x` (i.e., `↑(Real.sinh x)`) is equal to the complex hyperbolic sine of the complex number equivalent of `x` (i.e., `Complex.sinh ↑x`). In other words, the real hyperbolic sine function, when extended to complex numbers, behaves the same as the complex hyperbolic sine function. This theorem serves to bridge the behaviors of the hyperbolic sine function in real and complex domains.
More concisely: The real hyperbolic sine function and the complex hyperbolic sine function agree, i.e., `Complex.sinh ↑x = ↑(Real.sinh x)` for all real numbers `x`.
|
Complex.cos_zero
theorem Complex.cos_zero : Complex.cos 0 = 1
The theorem `Complex.cos_zero` states that the cosine of zero in the complex number system is equal to one. This is derived from the definition of the complex cosine function, which is defined in terms of the exponential function. In more mathematical terms, this theorem is stating that `cos(0) = 1` for complex numbers.
More concisely: The theorem asserts that the complex cosine of zero is equal to one, i.e., `cos(0) = 1` in the complex number system.
|
Complex.abs_exp_ofReal_mul_I
theorem Complex.abs_exp_ofReal_mul_I : ∀ (x : ℝ), Complex.abs (↑x * Complex.I).exp = 1
This theorem states that for all real numbers `x`, the absolute value (or magnitude) of the complex exponential function when evaluated at the product of `x` and the imaginary unit `I`, is equal to 1. In simpler terms, whenever we multiply a real number by the imaginary unit and then apply the complex exponential function to the result, the magnitude of the resulting complex number will always be 1. In mathematical notation, this theorem can be expressed as: for all x in ℝ, |exp(x * i)| = 1.
More concisely: For all real numbers x, |exp(xi)| = 1. (The complex exponential function of the product of a real number and the imaginary unit has magnitude 1.)
|
Complex.sin_add
theorem Complex.sin_add : ∀ (x y : ℂ), (x + y).sin = x.sin * y.cos + x.cos * y.sin
This theorem states that for any two complex numbers `x` and `y`, the sine of the sum (`x + y`) is equal to the product of the sine of `x` and the cosine of `y`, plus the product of the cosine of `x` and the sine of `y`. This mirrors the well-known trigonometric identity in real numbers, namely, $\sin(x + y) = \sin(x)\cos(y) + \cos(x)\sin(y)$, where $x$ and $y$ are real numbers. Here, the sine and cosine functions are defined for complex numbers via the exponential function.
More concisely: The theorem asserts that for complex numbers `x` and `y`, the sine of their sum equals the sum of the product of sine `x` and cosine `y`, and the product of cosine `x` and sine `y`. In Lean 4 notation, `sine (x + y) = sine x * cos y + cos x * sine y`.
|
Real.cosh_sq'
theorem Real.cosh_sq' : ∀ (x : ℝ), x.cosh ^ 2 = 1 + x.sinh ^ 2
This theorem states that for every real number `x`, the square of the hyperbolic cosine of `x` is equal to 1 plus the square of the hyperbolic sine of `x`. In mathematical notation, this is represented as: ∀x ∈ ℝ, cosh²(x) = 1 + sinh²(x). This is analogous to the well-known trigonometric identity involving the sine and cosine functions, but in the context of hyperbolic functions.
More concisely: For all real numbers x, the square of the hyperbolic cosine of x equals the sum of the squares of the hyperbolic sine and one: cosh²(x) = 1 + sinh²(x).
|
Complex.sinh_two_mul
theorem Complex.sinh_two_mul : ∀ (x : ℂ), (2 * x).sinh = 2 * x.sinh * x.cosh
The theorem `Complex.sinh_two_mul` states that for all complex numbers `x`, the hyperbolic sine of twice `x` is equal to twice the product of the hyperbolic sine of `x` and the hyperbolic cosine of `x`. In mathematical notation, it expresses the identity $\sinh(2x) = 2 \sinh(x) \cosh(x)$ for all complex numbers $x$.
More concisely: For all complex numbers x, $\sinh(2x) = 2\cdot\sinh(x)\cdot\cosh(x)$.
|
Complex.ofReal_sin_ofReal_re
theorem Complex.ofReal_sin_ofReal_re : ∀ (x : ℝ), ↑(↑x).sin.re = (↑x).sin
This theorem states that for all real numbers x, the real part of the complex sine of x, when promoted to a complex number, is equal to the complex sine of x. In other words, it asserts that the real component of the complex sine function, when applied to a real argument, fully captures the value of the complex sine function on that argument. This emphasizes the fact that the complex sine function reduces to the real sine function when applied to real numbers.
More concisely: The real part of the complex sine function equals the complex sine function for all real numbers.
|
Real.sin_le_one
theorem Real.sin_le_one : ∀ (x : ℝ), x.sin ≤ 1
This theorem states that for all real numbers `x`, the sine of `x` is less than or equal to 1. In other words, it asserts the well-known mathematical fact that the sine function always returns a value between -1 and 1 for any real number input.
More concisely: For all real numbers x, |sin(x)| ≤ 1.
|
Complex.ofReal_cos
theorem Complex.ofReal_cos : ∀ (x : ℝ), ↑x.cos = (↑x).cos
This theorem states that for all real numbers `x`, the complex number obtained by considering `Real.cos x` as a complex number is equal to the value of the complex cosine function evaluated at `x` considered as a complex number. In other words, when a real number is put into the real cosine function and then converted into a complex number, it gives the same result as if the real number was directly put into the complex cosine function.
More concisely: The real and complex cosine functions agree for real arguments: for all `x` in `ℝ`, `Complex.cos (convert x toComplex) = Real.cos x`.
|
Real.sinh_zero
theorem Real.sinh_zero : Real.sinh 0 = 0
This theorem states that the real hyperbolic sine of zero is zero. In mathematical terms, this can be written as $\sinh(0) = 0$. This is a property of the real hyperbolic sine function, which is defined as the real part of the complex hyperbolic sine.
More concisely: The real hyperbolic sine function evaluates to zero at zero: $\sinh(0) = 0$.
|
Real.cosh_pos
theorem Real.cosh_pos : ∀ (x : ℝ), 0 < x.cosh
The theorem `Real.cosh_pos` states that the real hyperbolic cosine function, represented as `Real.cosh`, is always positive for any real number `x`. In other words, for every real number `x`, the value of `Real.cosh x` is greater than 0.
More concisely: For all real numbers x, Real.cosh x > 0.
|
Real.sin_add
theorem Real.sin_add : ∀ (x y : ℝ), (x + y).sin = x.sin * y.cos + x.cos * y.sin
This theorem, `Real.sin_add`, states that for all real numbers `x` and `y`, the sine of the sum (`x + y`) is equal to the product of the sine of `x` and the cosine of `y`, plus the product of the cosine of `x` and the sine of `y`. In mathematical terms, it can be written as $\sin(x+y) = \sin(x)\cos(y) + \cos(x)\sin(y)$. This is a well-known trigonometric identity often used in the study of oscillations, waves, and many other areas of mathematics and physics.
More concisely: The sine function is additive, that is, $\sin(x + y) = \sin(x)\cos(y) + \cos(x)\sin(y)$.
|
Real.exp_eq_exp
theorem Real.exp_eq_exp : ∀ {x y : ℝ}, x.exp = y.exp ↔ x = y
The theorem `Real.exp_eq_exp` states that for all real numbers `x` and `y`, the exponential function `Real.exp` of `x` and `y` are equal if and only if `x` and `y` themselves are equal. In other words, the real exponential function is injective (or one-to-one) on the set of real numbers.
More concisely: The real exponential function is injective (one-to-one): for all real numbers x and y, Real.exp x = Real.exp y if and only if x = y.
|
Real.cos_zero
theorem Real.cos_zero : Real.cos 0 = 1
This theorem states that the cosine of zero in real numbers is equal to one. In other words, if we apply the `Real.cos` function to `0`, the result is `1`. This corresponds to the well-known fact from trigonometry that $\cos(0) = 1$.
More concisely: The cosine of 0 in the real numbers is equal to 1. (cos 0 = 1 in real numbers)
|
Real.sinh_add_cosh
theorem Real.sinh_add_cosh : ∀ (x : ℝ), x.sinh + x.cosh = x.exp
The theorem states that for all real numbers `x`, the sum of the real hyperbolic sine of `x` and the real hyperbolic cosine of `x` is equal to the real exponential of `x`. In mathematical terms, this can be written as $\sinh(x) + \cosh(x) = e^x$ for all $x \in \mathbb{R}$.
More concisely: For all real numbers x, $\sinh(x) + \cosh(x) = e^x$.
|
Real.cos_add
theorem Real.cos_add : ∀ (x y : ℝ), (x + y).cos = x.cos * y.cos - x.sin * y.sin
This theorem states that for all real numbers `x` and `y`, the cosine of the sum of `x` and `y` is equal to the product of the cosine of `x` and the cosine of `y` minus the product of the sine of `x` and the sine of `y`. This is a formalization of the well-known trigonometric identity $\cos(a + b) = \cos(a)\cos(b) - \sin(a)\sin(b)$.
More concisely: The cosine of the sum of two real numbers is equal to the product of their cosines minus the product of their sines.
|
Complex.cos_ofReal_im
theorem Complex.cos_ofReal_im : ∀ (x : ℝ), (↑x).cos.im = 0
This theorem states that for every real number `x`, the imaginary part of the complex cosine of `x` is zero. In other words, if you take any real number, convert it to a complex number (by treating it as the real part and adding zero as the imaginary part), and take the cosine of that complex number, the imaginary part of the result will always be zero. This is consistent with the usual definition of the cosine function on the real numbers, which always returns a real number.
More concisely: For all real numbers x, the complex cosine of x has zero imaginary part.
|
Complex.cosh_add
theorem Complex.cosh_add : ∀ (x y : ℂ), (x + y).cosh = x.cosh * y.cosh + x.sinh * y.sinh
This theorem states that for any two complex numbers `x` and `y`, the hyperbolic cosine of the sum of `x` and `y`, denoted `Complex.cosh (x + y)`, is equal to the product of the hyperbolic cosine of `x` and the hyperbolic cosine of `y` plus the product of the hyperbolic sine of `x` and the hyperbolic sine of `y`. In mathematical notation, this would be expressed as `cosh(x + y) = cosh(x) * cosh(y) + sinh(x) * sinh(y)`. This is a complex number analogue of the classical addition formula for the hyperbolic cosine function.
More concisely: The hyperbolic cosine of the sum of two complex numbers is equal to the product of their hyperbolic cosines plus the product of their hyperbolic sines. In Lean notation: `Complex.cosh (x + y) = cosh x * cosh y + sinh x * sinh y`.
|
Real.sinh_eq
theorem Real.sinh_eq : ∀ (x : ℝ), x.sinh = (x.exp - (-x).exp) / 2
This theorem defines the hyperbolic sine function (`sinh`) for any real number `x`. It states that the `sinh` of `x` is equal to the difference of the exponential of `x` and the exponential of `-x`, all divided by 2. In mathematical terms, for any real number `x`, `sinh(x)` equals `(e^x - e^(-x))/2`.
More concisely: The hyperbolic sine function is defined as `sinh(x) = (e^x - e^(-x))/2`.
|
Real.exp_lt_one_iff
theorem Real.exp_lt_one_iff : ∀ {x : ℝ}, x.exp < 1 ↔ x < 0
The theorem `Real.exp_lt_one_iff` states that for all real numbers `x`, the exponential of `x` is less than 1 if and only if `x` is less than 0. In other words, this theorem establishes a bi-conditional relationship between a real number being less than 0 and its exponential value being less than 1.
More concisely: For all real numbers x, exp(x) < 1 if and only if x < 0.
|
Real.exp_neg
theorem Real.exp_neg : ∀ (x : ℝ), (-x).exp = x.exp⁻¹
The theorem `Real.exp_neg` states that for all real numbers `x`, the exponential function evaluated at the negative of `x` is equal to the inverse of the exponential function evaluated at `x`. In mathematical notation, this can be written as: for all $x \in \mathbb{R}$, $\exp(-x) = \exp(x)^{-1}$. This is a fundamental property of the exponential function.
More concisely: The exponential function's value with a negative real number argument is equal to the reciprocal of the exponential function's value with the same positive real number argument. (i.e., for all $x \in \mathbb{R}$, $\exp(-x) = \exp(x)^{-1}$)
|
Complex.tan_zero
theorem Complex.tan_zero : Complex.tan 0 = 0
This theorem states that the value of the complex tangent function at zero is zero. In other words, when you take the tangent of zero in the complex number system (which is defined as the complex sine of the number divided by the complex cosine of the number), the result is zero.
More concisely: The complex tangent function evaluates to zero at zero. (tan(z) = z / komplex_abs z where z is a complex number and komplex_abs is the absolute value function in Lean 4 complex arithmetic.)
|
Mathlib.Data.Complex.Exponential._auxLemma.7
theorem Mathlib.Data.Complex.Exponential._auxLemma.7 : ∀ (x : ℝ), (↑x).sin = ↑x.sin
This theorem states that for any real number `x`, the complex sine of `x` is equal to the real part of the sine of `x`. In other words, the sine function, when applied to a real number and considered as a complex function, gives a result that has its real part equal to the sine of that number computed in the real numbers. This theorem essentially explains the relationship between the complex sine function and the real sine function.
More concisely: The theorem asserts that for all real numbers x, the complex sine function's real part is equal to the real sine of x. In other words, Re(sin(x + i0)) = sin(x).
|
Complex.sin_zero
theorem Complex.sin_zero : Complex.sin 0 = 0
This theorem states that the sine of zero in the complex number system is zero. In other words, when we apply the complex sine function, as defined through the exponential function, to the number zero, the result is zero.
More concisely: The complex sine function evaluates to zero at zero. (sin(0) = 0 in the complex numbers)
|
Complex.sin_neg
theorem Complex.sin_neg : ∀ (x : ℂ), (-x).sin = -x.sin
This theorem states that the complex sine function has odd symmetry. Specifically, for any complex number `x`, the sine of negative `x` is equal to the negative of the sine of `x`. In mathematical notation, this would be expressed as sin(-x) = -sin(x) for all complex numbers `x`.
More concisely: The sine function is odd, that is, sin(-x) = -sin(x) for all complex numbers x.
|
Complex.cosh_conj
theorem Complex.cosh_conj : ∀ (x : ℂ), ((starRingEnd ℂ) x).cosh = (starRingEnd ℂ) x.cosh
The theorem `Complex.cosh_conj` states that for any complex number `x`, the complex hyperbolic cosine of the conjugate of `x` is equal to the conjugate of the complex hyperbolic cosine of `x`. In other words, the complex hyperbolic cosine function commutes with complex conjugation. This can be expressed in mathematical notation as: for all $x \in \mathbb{C}$, $\cosh(\overline{x}) = \overline{\cosh(x)}$.
More concisely: The complex hyperbolic cosine function commutes with complex conjugation, i.e., for all complex numbers x, $\cosh(\overline{x}) = \overline{\cosh(x)}$.
|
Real.abs_exp
theorem Real.abs_exp : ∀ (x : ℝ), |x.exp| = x.exp
This theorem states that the absolute value of the exponential function, when applied to any real number `x`, is equal to the value of the exponential function at `x` itself. In mathematical terms, for any real number `x`, the equality `|exp(x)| = exp(x)` holds true. This implies that the real exponential function always returns a non-negative number.
More concisely: For all real numbers x, the absolute value of the exponential function |exp(x)| equals exp(x).
|
Complex.cosh_neg
theorem Complex.cosh_neg : ∀ (x : ℂ), (-x).cosh = x.cosh
This theorem states that the complex hyperbolic cosine function has even symmetry. In other words, for any complex number `x`, the value of the hyperbolic cosine of `-x` is the same as the hyperbolic cosine of `x`. This mirrors the property of the real hyperbolic cosine function, which is also an even function.
More concisely: The complex hyperbolic cosine function is an even function, i.e., cosh(-x) = cosh(x) for all complex numbers x.
|
Complex.sinh_neg
theorem Complex.sinh_neg : ∀ (x : ℂ), (-x).sinh = -x.sinh
This theorem states that the complex hyperbolic sine function, `Complex.sinh`, satisfies the property of oddness. Specifically, for any complex number `x`, the value of `Complex.sinh` at `-x` is equal to the negation of the value of `Complex.sinh` at `x`. In mathematical language, this can be written as sinh(-x) = -sinh(x) for all complex numbers x.
More concisely: The complex hyperbolic sine function satisfies the property of oddness, that is, sinh(-x) = -sinh(x) for all complex numbers x.
|
Real.sin_sq_add_cos_sq
theorem Real.sin_sq_add_cos_sq : ∀ (x : ℝ), x.sin ^ 2 + x.cos ^ 2 = 1
This theorem states that for any real number `x`, the square of the sine of `x` plus the square of the cosine of `x` equals 1. In other words, it is the real-number version of the Pythagorean trigonometric identity: $\sin^2(x) + \cos^2(x) = 1$ for all real numbers `x`.
More concisely: For all real numbers x, the sum of the squares of sine and cosine of x is equal to 1: $\sin^2(x) + \cos^2(x) = 1$.
|
Real.exp_add
theorem Real.exp_add : ∀ (x y : ℝ), (x + y).exp = x.exp * y.exp
The `Real.exp_add` theorem states that for all real numbers `x` and `y`, the exponential of the sum `x + y` is equal to the product of the exponentials of `x` and `y`. In mathematical notation, this can be written as $e^{x+y} = e^x * e^y$. This corresponds to the well known property of exponentiation in the field of real numbers.
More concisely: The `Real.exp_add` theorem asserts that for all real numbers `x` and `y`, $e^{x+y} = e^x \cdot e^y$.
|
Complex.tan_neg
theorem Complex.tan_neg : ∀ (x : ℂ), (-x).tan = -x.tan
This theorem states that the complex tangent function is an odd function. Specifically, for any complex number `x`, the value of the complex tangent of `-x` is equal to the negation of the complex tangent of `x`. In mathematical notation, this can be written as `tan(-x) = -tan(x)`.
More concisely: The complex tangent function is an odd function, that is, `tan(-x) = -tan(x)` for all complex numbers `x`.
|
Complex.cosh_two_mul
theorem Complex.cosh_two_mul : ∀ (x : ℂ), (2 * x).cosh = x.cosh ^ 2 + x.sinh ^ 2
The theorem named `Complex.cosh_two_mul` states that for all complex numbers `x`, the complex hyperbolic cosine of `2 * x` is equal to the sum of the squares of the complex hyperbolic cosine and the complex hyperbolic sine of `x`. In mathematical terms, it states that for every complex number `x`, $\cosh(2x) = \cosh^2(x) + \sinh^2(x)$. This is a complex number version of the double-angle formula in hyperbolic trigonometry.
More concisely: The complex hyperbolic cosine of twice a complex number equals the sum of the squares of its hyperbolic cosine and hyperbolic sine. In mathematical notation, $\cosh(2x) = \cosh^2(x) + \sinh^2(x)$.
|
Complex.ofReal_cosh
theorem Complex.ofReal_cosh : ∀ (x : ℝ), ↑x.cosh = (↑x).cosh
This theorem states that for every real number `x`, the complex number that is the result of mapping `x` through the real hyperbolic cosine function `Real.cosh` and then considering this result as a complex number (done by `↑(Real.cosh x)`) is equal to the complex hyperbolic cosine of `x` considered as a complex number (`Complex.cosh ↑x`). In other words, the real hyperbolic cosine `Real.cosh` function, when lifted to the complex numbers, coincides with the `Complex.cosh` function on the real line.
More concisely: For every real number `x`, `Complex.cosh (Real.toComplex x) = ↑(Real.cosh x)`.
|
Real.exp_sub
theorem Real.exp_sub : ∀ (x y : ℝ), (x - y).exp = x.exp / y.exp
The theorem `Real.exp_sub` states that for any two real numbers `x` and `y`, the exponential function of the difference `(x - y)` is equal to the quotient of the exponential function of `x` divided by the exponential function of `y`. This is expressed mathematically as: for all real numbers x and y, `exp(x - y) = exp(x) / exp(y)`, where `exp` denotes the real exponential function.
More concisely: The real exponential function satisfies the property `exp(x - y) = exp(x) / exp(y)` for all real numbers `x` and `y`.
|
Real.inv_one_add_tan_sq
theorem Real.inv_one_add_tan_sq : ∀ {x : ℝ}, x.cos ≠ 0 → (1 + x.tan ^ 2)⁻¹ = x.cos ^ 2
This theorem states that for any real number `x`, as long as the cosine of `x` is not zero, the reciprocal of the quantity `(1 + tangent of x squared)` is equal to the square of the cosine of `x`. In mathematical terms, it asserts that for any $x \in \mathbb{R}$ with $\cos(x) \neq 0$, we have $(1 + \tan^2(x))^{-1} = \cos^2(x)$.
More concisely: For any real number $x$ with non-zero cosine, the reciprocal of $(1 + \tan^2(x))$ equals the square of the cosine: $(1 + \tan^2(x))^{-1} = \cos^2(x)$.
|
Complex.two_cosh
theorem Complex.two_cosh : ∀ (x : ℂ), 2 * x.cosh = x.exp + (-x).exp
The theorem `Complex.two_cosh` states that for any complex number `x`, twice the complex hyperbolic cosine of `x` is equal to the sum of the complex exponential of `x` and the complex exponential of the negation of `x`. In mathematical terms, this can be written as: for all `x` in the complex numbers, `2 * cosh(x) = exp(x) + exp(-x)`. This is a complex number version of the familiar identity from real number hyperbolic trigonometry.
More concisely: For all complex numbers `x`, `2 * cosh(x) = exp(x) + exp(-x)`.
|
Complex.ofReal_sin
theorem Complex.ofReal_sin : ∀ (x : ℝ), ↑x.sin = (↑x).sin
This theorem states that for all real numbers `x`, casting the real sine of `x` to a complex number yields the same result as calculating the complex sine of `x` cast to a complex number. In other words, the real sine function, when extended to the complex numbers, coincides with the complex sine function on the real line. Mathematically, this is expressed as ∀x ∈ ℝ: `Real.sin(x)` = `Complex.sin(x)`.
More concisely: The real and complex sine functions agree on the real numbers: `Real.sin(x) = Complex.sin(x)` for all `x ∈ ℝ`.
|
Real.tan_eq_sin_div_cos
theorem Real.tan_eq_sin_div_cos : ∀ (x : ℝ), x.tan = x.sin / x.cos
This theorem states that for all real numbers `x`, the value of the tangent of `x` is equal to the value of the sine of `x` divided by the cosine of `x`. In other words, `tan(x) = sin(x) / cos(x)`. This is a well-known identity from trigonometry which holds for all real numbers.
More concisely: The tangent function is equal to the quotient of the sine and cosine functions for all real numbers. (tan(x) = sin(x) / cos(x))
|