Complex.hasStrictDerivAt_cosh
theorem Complex.hasStrictDerivAt_cosh : ∀ (x : ℂ), HasStrictDerivAt Complex.cosh x.sinh x
The theorem `Complex.hasStrictDerivAt_cosh` states that the complex hyperbolic cosine function, denoted as `Complex.cosh`, is strictly differentiable at every point `x` in the complex plane. The derivative of this function at any point `x` is given by the complex hyperbolic sine function evaluated at that point, which is `Complex.sinh x`. Strict differentiability here implies that the difference between the function values at two points approaches the product of the difference of the points and the derivative, plus a term that becomes negligible, as the two points converge to `x`.
More concisely: The complex hyperbolic cosine function `Complex.cosh` is strictly differentiable on the complex plane with derivative `Complex.sinh`.
|
Real.hasDerivAt_sin
theorem Real.hasDerivAt_sin : ∀ (x : ℝ), HasDerivAt Real.sin x.cos x
This theorem states that for all real numbers `x`, the function `Real.sin` (representing the real sine function) has its derivative at the point `x`, and this derivative is `Real.cos x` (the real cosine function evaluated at `x`). In mathematical terms, it says that the derivative of the sine function at any point is the cosine function at that point, which is a well-known property in calculus.
More concisely: The derivative of the real sine function is the real cosine function.
|
Real.hasStrictDerivAt_sin
theorem Real.hasStrictDerivAt_sin : ∀ (x : ℝ), HasStrictDerivAt Real.sin x.cos x
This theorem states that for all real numbers `x`, the function `Real.sin`, which represents the real sine function, has a strict derivative at the point `x`. The derivative is given by `Real.cos x`, which represents the real cosine function. This means that the change in the sine function at any point `x` is best represented by the value of the cosine function at that same point, with the change becoming arbitrarily close as the difference in points approaches zero. In the mathematical notation, this would be expressed as `f'(x) = cos(x)` for `f(x) = sin(x)`.
More concisely: The real sine function has a strict derivative equal to the real cosine function at every real number.
|
Complex.contDiff_cosh
theorem Complex.contDiff_cosh : ∀ {n : ℕ∞}, ContDiff ℂ n Complex.cosh
This theorem states that the complex hyperbolic cosine function, `Complex.cosh`, is continuously differentiable for all natural numbers `n`, including infinity (`ℕ∞`). The function `Complex.cosh` is defined as the average of the exponential function evaluated at a complex number `z` and its negation. The continuous differentiability means that the function has derivatives of all orders up to `n` and that these derivatives vary smoothly.
More concisely: The complex hyperbolic cosine function `Complex.cosh : ℂ → ℂ`, defined as the average of `exp` and its negation, is continuously differentiable for all natural numbers `n` including infinity.
|
Real.contDiff_cosh
theorem Real.contDiff_cosh : ∀ {n : ℕ∞}, ContDiff ℝ n Real.cosh
The theorem `Real.contDiff_cosh` states that for all `n`, which is a natural number or infinity (`ℕ∞`), the real hyperbolic cosine function (`Real.cosh`) is continuously differentiable of order `n`. In other words, the hyperbolic cosine function can be differentiated `n` times and the result is a continuous function.
More concisely: For all natural numbers or infinity `n`, the `n`-th derivative of the real hyperbolic cosine function is a continuous function.
|
Complex.hasStrictDerivAt_sin
theorem Complex.hasStrictDerivAt_sin : ∀ (x : ℂ), HasStrictDerivAt Complex.sin x.cos x
The theorem `Complex.hasStrictDerivAt_sin` states that the complex sine function is strictly differentiable at every point in the complex plane. Furthermore, the derivative of the complex sine function at any point `x` is given by the complex cosine function evaluated at `x`. In mathematical terms, this is written as `f'(x) = cos(x)` for the complex sine function `f(x)`.
More concisely: The complex sine function is complex differentiable with derivative equal to the complex cosine function at every point in the complex plane.
|
Real.deriv_sin
theorem Real.deriv_sin : deriv Real.sin = Real.cos
This theorem states that the derivative of the real sine function equals the real cosine function. In mathematical terms, if `f(x) = sin(x)` for a real number `x`, then the derivative of `f` with respect to `x`, denoted as `f'(x)`, is equal to `cos(x)`. This fact is a well-known result in calculus.
More concisely: The derivative of the real sine function is equal to the real cosine function. (i.e., sin'(x) = cos(x) for all x in R)
|
Complex.hasDerivAt_sin
theorem Complex.hasDerivAt_sin : ∀ (x : ℂ), HasDerivAt Complex.sin x.cos x
This theorem states that the complex sine function is differentiable at every point. Specifically, the derivative of the complex sine function at any point `x` in the complex numbers, is given by the complex cosine function evaluated at that point `x`.
More concisely: The complex sine function is complex differentiable, with derivative equal to the complex conjugate of the complex cosine function at each point in the complex numbers.
|
Real.sinh_strictMono
theorem Real.sinh_strictMono : StrictMono Real.sinh
This theorem states that the real hyperbolic sine function, denoted as `sinh`, is strictly monotone. In other words, if `a` and `b` are real numbers such that `a < b`, then `sinh(a) < sinh(b)`. This means that as you move from left to right on the real number line, the values of the `sinh` function strictly increase.
More concisely: The real hyperbolic sine function is strictly increasing.
|
Real.contDiff_sinh
theorem Real.contDiff_sinh : ∀ {n : ℕ∞}, ContDiff ℝ n Real.sinh
This theorem states that the real hyperbolic sine function, defined as the real part of the complex hyperbolic sine, is continuously differentiable for all natural numbers `n`, including infinity. In mathematical terms, it verifies that the function `Real.sinh : ℝ → ℝ` is `n`-times continuously differentiable for every `n` in `ℕ∞`, where `ℕ∞` is the set of natural numbers extended by infinity.
More concisely: The real hyperbolic sine function, defined as the real part of the complex hyperbolic sine, is continuously differentiable for all natural numbers and infinity. Equivalently, `Real.sinh : ℝ → ℝ` is `n`-times differentiable for every `n` in `ℕ ∪ {∞}`.
|
Complex.hasDerivAt_sinh
theorem Complex.hasDerivAt_sinh : ∀ (x : ℂ), HasDerivAt Complex.sinh x.cosh x
The theorem states that the complex hyperbolic sine function, defined as `(Complex.exp z - Complex.exp (-z)) / 2`, is differentiable at every point in the complex plane. Furthermore, the derivative of the complex hyperbolic sine function at any point `x` is given by the complex hyperbolic cosine function at that point, which is defined as `(Complex.exp z + Complex.exp (-z)) / 2`.
More concisely: The complex hyperbolic sine function, defined as (exp z - exp (-z)) / 2, is a complex differentiable function with derivative given by the complex hyperbolic cosine function (exp z + exp (-z)) / 2.
|
Real.contDiff_sin
theorem Real.contDiff_sin : ∀ {n : ℕ∞}, ContDiff ℝ n Real.sin
This theorem states that the real sine function is continuously differentiable for any natural number `n`, including infinity. In other words, you can take the derivative of the real sine function any number of times (possibly infinite) and the resulting functions are all continuous. This property is often symbolized in mathematics as `Real.sin ∈ Cⁿ(ℝ) for all n ∈ ℕ ∪ {∞}`.
More concisely: The real sine function belongs to the class of continuously differentiable functions of order `n` on the real numbers for every natural number `n` and infinity.
|
Real.sinh_injective
theorem Real.sinh_injective : Function.Injective Real.sinh
The theorem `Real.sinh_injective` states that the real hyperbolic sine function (denoted as `Real.sinh`) is injective. This means that for any two real numbers `a` and `b`, if the hyperbolic sine of `a` is equal to the hyperbolic sine of `b` (expressed in Lean 4 as `sinh a = sinh b`), then `a` must be equal to `b` (expressed as `a = b`). In other words, no two different real numbers can have the same hyperbolic sine value.
More concisely: The real hyperbolic sine function is a bijection (injective and surjective function). In other words, for all real numbers `a` and `b`, `sinh a = sinh b` implies `a = b`.
|
Real.contDiff_cos
theorem Real.contDiff_cos : ∀ {n : ℕ∞}, ContDiff ℝ n Real.cos
The theorem `Real.contDiff_cos` states that the cosine function, which maps real numbers to real numbers, is continuously differentiable for all natural number orders `n`, inclusive of infinity. Here, continuously differentiable means that the function's `n`-th derivative exists and is continuous. The type `ℕ∞` is used to denote the set of nonnegative integers, including infinity.
More concisely: The cosine function is continuously differentiable for all natural number orders. That is, for all natural numbers `n` including infinity, the `n`-th derivative of `cos` exists and is a continuous function.
|
Complex.hasDerivAt_cos
theorem Complex.hasDerivAt_cos : ∀ (x : ℂ), HasDerivAt Complex.cos (-x.sin) x
This theorem states that the complex cosine function, which is defined via the exponential function, is differentiable at every point in its domain. More specifically, the derivative of the complex cosine function at any point `x` is given by the negative of the complex sine function at that same point `x`.
More concisely: The complex cosine function, defined as the real part of the complex exponential function, is differentiable with derivative given by the negative complex sine function.
|
Real.hasDerivAt_cosh
theorem Real.hasDerivAt_cosh : ∀ (x : ℝ), HasDerivAt Real.cosh x.sinh x
The theorem `Real.hasDerivAt_cosh` states that for any real number `x`, the derivative of the hyperbolic cosine function (`Real.cosh`) at the point `x` is equal to the value of the hyperbolic sine function (`Real.sinh`) at that same point `x`. In other words, if we differentiate the hyperbolic cosine function at any real number, we will get the hyperbolic sine function evaluated at that number. This corresponds to the mathematical statement $\frac{d}{dx}\cosh(x) = \sinh(x)$ in calculus.
More concisely: The derivative of the hyperbolic cosine function equals the hyperbolic sine function. In Lean: `Real.hasDerivAt_cosh : ∀ x : ℝ, (derivative (Real.cosh) x) = Real.sinh x`.
|
Real.deriv_cos'
theorem Real.deriv_cos' : deriv Real.cos = fun x => -x.sin
The theorem `Real.deriv_cos'` states that the derivative of the real cosine function is negative of the real sine function. In other words, if you take any real number `x` and calculate the derivative of the cosine function at `x`, the result will be the negative of the sine of `x`. This is a well-known result in calculus which can be expressed in the form (d/dx) cos(x) = -sin(x).
More concisely: The derivative of the real cosine function is equal to the negative of the real sine function.
|
Complex.hasDerivAt_cosh
theorem Complex.hasDerivAt_cosh : ∀ (x : ℂ), HasDerivAt Complex.cosh x.sinh x
The theorem states that the complex hyperbolic cosine function is differentiable at every point in the complex plane. Moreover, the derivative of the complex hyperbolic cosine function at any point 'x' in the complex plane is given by the value of the complex hyperbolic sine function at that point.
More concisely: The complex hyperbolic cosine function has a complex differentiable derivative equal to the complex hyperbolic sine function at every point in the complex plane.
|
Real.sinh_le_sinh
theorem Real.sinh_le_sinh : ∀ {x y : ℝ}, x.sinh ≤ y.sinh ↔ x ≤ y
This theorem states that for any two real numbers `x` and `y`, the real hyperbolic sine of `x` is less than or equal to the real hyperbolic sine of `y` if and only if `x` is less than or equal to `y`. This establishes the order preservation property of the real hyperbolic sine function.
More concisely: The real hyperbolic sine function is order-preserving: for all real numbers x and y, sinh(x) ≤ sinh(y) if and only if x ≤ y.
|
Real.hasDerivAt_cos
theorem Real.hasDerivAt_cos : ∀ (x : ℝ), HasDerivAt Real.cos (-x.sin) x
This theorem states that for any real number `x`, the function `Real.cos` (the cosine function on the real numbers) has a derivative at the point `x`, and the derivative is `-Real.sin x` (the negation of the sine of `x`). In other words, the derivative of the cosine function at any point is the negative of the sine function at that same point, which is consistent with calculus theory.
More concisely: The derivative of the cosine function on the real numbers is equal to the negative of the sine function.
|
Complex.contDiff_cos
theorem Complex.contDiff_cos : ∀ {n : ℕ∞}, ContDiff ℂ n Complex.cos
This theorem asserts that for every non-negative integer `n`, possibly extended to infinity, the complex cosine function `Complex.cos` is `n` times continuously differentiable. In mathematical terms, it means the complex cosine function, defined as $$Complex.cos(z) = \frac{Complex.exp (z * Complex.I) + Complex.exp (-z * Complex.I)}{2},$$ has continuous derivatives of all orders up to `n`, where `Complex.I` is the imaginary unit in complex numbers, and `Complex.exp` is the complex exponential function.
More concisely: The complex cosine function, defined as (Complex.exp (z * Complex.I) + Complex.exp (-z * Complex.I) / 2), is infinitely differentiable.
|
Complex.contDiff_sin
theorem Complex.contDiff_sin : ∀ {n : ℕ∞}, ContDiff ℂ n Complex.sin
This theorem states that the complex sine function, which is defined as `(Complex.exp (-z * Complex.I) - Complex.exp (z * Complex.I)) * Complex.I / 2`, is continuously differentiable for all orders of differentiation. In other words, the function's derivatives of all orders exist and are continuous in the domain of complex numbers. Here, `n` represents the order of differentiation and can be any natural number or infinity (`ℕ∞`), and `ContDiff ℂ n Complex.sin` is a statement that the function `Complex.sin` is `n`-times continuously differentiable in the field of complex numbers.
More concisely: The complex sine function, defined as (exp(-z * I) - exp(z * I)) * I / 2, is continuously differentiable to all orders in the complex numbers domain.
|
Real.hasDerivAt_sinh
theorem Real.hasDerivAt_sinh : ∀ (x : ℝ), HasDerivAt Real.sinh x.cosh x
This theorem states that for all real numbers `x`, the function `Real.sinh` (the real hyperbolic sine function) has a derivative at the point `x`. The derivative of `Real.sinh` at the point `x` is given by `Real.cosh x` (the real hyperbolic cosine function evaluated at `x`). This means that `Real.cosh` is the rate of change of `Real.sinh` at any given point `x` in its domain.
More concisely: The real hyperbolic sine function `Real.sinh` has a derivative equal to the real hyperbolic cosine function `Real.cosh` at every real number `x`.
|
Complex.contDiff_sinh
theorem Complex.contDiff_sinh : ∀ {n : ℕ∞}, ContDiff ℂ n Complex.sinh
This theorem states that the complex hyperbolic sine function, `Complex.sinh`, is continuously differentiable for all orders `n` in the extended natural numbers, denoted as `ℕ∞`. In other words, you can take the derivative of `Complex.sinh` as many times as you want, and the resulting function will still be continuous. This is a fundamental property of the complex hyperbolic sine function and is essential in many areas of mathematics and engineering.
More concisely: The complex hyperbolic sine function, `Complex.sinh`, is continuously differentiable for all orders on the extended natural numbers, `ℕ∞`.
|
Complex.hasStrictDerivAt_sinh
theorem Complex.hasStrictDerivAt_sinh : ∀ (x : ℂ), HasStrictDerivAt Complex.sinh x.cosh x
The theorem states that the complex hyperbolic sine function, which is denoted by `Complex.sinh`, is strictly differentiable at every point in the complex plane. Furthermore, the derivative of `Complex.sinh` at any point `x` in the complex plane is given by the complex hyperbolic cosine function evaluated at that point, i.e., `Complex.cosh x`. Strict differentiability means that the difference between the function values at two points approaches the derivative times the difference in points plus a term that goes to zero faster than the difference in points, as the two points approach each other.
More concisely: The complex hyperbolic sine function `Complex.sinh` is strictly differentiable with derivative `Complex.cosh` throughout the complex plane.
|
Complex.hasStrictDerivAt_cos
theorem Complex.hasStrictDerivAt_cos : ∀ (x : ℂ), HasStrictDerivAt Complex.cos (-x.sin) x
The theorem `Complex.hasStrictDerivAt_cos` states that the complex cosine function is strictly differentiable at all points in the complex plane. The derivative at any point `x` in the complex plane is given by the negative of the complex sine of `x`, i.e., `-sin(x)`.
More concisely: The complex cosine function is strictly differentiable with derivative $-i\sin(x)$ for all complex numbers $x$.
|