Real.hasStrictDerivAt_exp
theorem Real.hasStrictDerivAt_exp : ∀ (x : ℝ), HasStrictDerivAt Real.exp x.exp x
This theorem states that the real exponential function has a strict derivative at any real number `x`. The value of this derivative at any point `x` happens to be the value of the exponential function at `x` itself. In mathematical terms, we can write this as `d/dx exp(x) = exp(x)` for all `x` in ℝ (the set of all real numbers). This means that the rate of change of the function `exp(x)` at any point `x` is equal to the value of the function at that point. This key property is one of the defining characteristics of the exponential function.
More concisely: The real exponential function has a derivative equal to itself at every real number: `d/dx (exp x) = exp x`.
|
Complex.hasStrictDerivAt_exp
theorem Complex.hasStrictDerivAt_exp : ∀ (x : ℂ), HasStrictDerivAt Complex.exp x.exp x
This theorem states that, for every complex number `x`, the complex exponential function `Complex.exp` has a strict derivative at the point `x`, and this derivative is itself `Complex.exp x`. In mathematical terms, this means that the rate of change of the complex exponential function at any point `x` is equal to the value of the complex exponential function at that point. The notion of strict differentiability used here implies that the difference between the function values at two nearby points `y` and `z` tends to be proportional to the difference `y - z`, with the factor of proportionality given by the derivative, plus a term that goes to zero faster than `y - z` as `y, z → x`.
More concisely: The complex exponential function `Complex.exp` is its own strict derivative.
|
Complex.differentiable_exp
theorem Complex.differentiable_exp :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ], Differentiable 𝕜 Complex.exp := by
sorry
The theorem `Complex.differentiable_exp` asserts that for any type '𝕜' which forms a non-trivially normed field and is also a normed algebra over the complex numbers, the complex exponential function (defined via its Taylor series) is differentiable at every point. In other words, the derivative of the complex exponential function exists for all points in its domain, under the conditions specified for '𝕜'.
More concisely: The complex exponential function, defined via its Taylor series, is differentiable for all complex numbers in the domain of any non-trivially normed field that is also a normed algebra over the complex numbers.
|
Complex.contDiff_exp
theorem Complex.contDiff_exp :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {n : ℕ∞},
ContDiff 𝕜 n Complex.exp
This theorem states that for any non-trivial normed field `𝕜` with a normed algebra structure over the complex numbers, the complex exponential function is continuously differentiable any number of times `n`, where `n` could be a natural number or infinity. In mathematical terms, the theorem asserts that the complex exponential function is `𝕜`-smooth.
More concisely: The complex exponential function is continuously differentiable an arbitrary number of times in any non-trivial normed field with a normed algebra structure over the complex numbers.
|
ContDiff.cexp
theorem ContDiff.cexp :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {n : ℕ∞},
ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => (f x).exp
This theorem states that for any nontrivial normed field `𝕜`, which also has a normed algebra structure over the complex numbers, and for any normed additive commutative group `E` with a normed space structure over `𝕜`, if a function `f` from `E` to the complex numbers is `n` times continuously differentiable, then the function that sends `x` to the complex exponential of `f(x)` is also `n` times continuously differentiable.
More concisely: If `𝕜` is a nontrivial normed field with a normed algebra structure over the complex numbers, `E` is a normed additive commutative group with a normed space structure over `𝕜`, and `f : E -> ℂ` is `n`-times continuously differentiable, then the function `x => exp(f(x))` is also `n`-times continuously differentiable.
|
Complex.hasDerivAt_exp
theorem Complex.hasDerivAt_exp : ∀ (x : ℂ), HasDerivAt Complex.exp x.exp x
The theorem `Complex.hasDerivAt_exp` states that the complex exponential function is differentiable at every point in the complex plane, and furthermore, the derivative of the complex exponential function at any point is the value of the complex exponential function at that point. In other words, for all complex numbers `x`, the derivative of `Complex.exp` at `x` is `Complex.exp x`.
More concisely: The complex exponential function is complex differentiable, and its derivative equals the complex exponential function itself.
|
Real.hasDerivAt_exp
theorem Real.hasDerivAt_exp : ∀ (x : ℝ), HasDerivAt Real.exp x.exp x
This theorem states that for any real number `x`, the function `Real.exp`, which represents the real exponential function, has a derivative at the point `x`. Furthermore, the derivative of `Real.exp` at `x` is simply `Real.exp x`. In other words, the derivative of the exponential function at any point is the exponential of that point itself.
More concisely: The real exponential function `Real.exp` has derivative equal to itself at any real number `x`.
|
Real.contDiff_exp
theorem Real.contDiff_exp : ∀ {n : ℕ∞}, ContDiff ℝ n Real.exp
This theorem states that for all natural numbers `n` extended to infinity, the real exponential function `Real.exp` is continuously differentiable `n` times. In mathematical terms, it means that the derivative of any order of the exponential function exists and is continuous on the real numbers.
More concisely: The real exponential function `Real.exp` is continuously differentiable to all orders on the real numbers.
|