hasStrictFDerivAt_exp_of_mem_ball
theorem hasStrictFDerivAt_exp_of_mem_ball :
β {π : Type u_1} {πΈ : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedCommRing πΈ]
[inst_2 : NormedAlgebra π πΈ] [inst_3 : CompleteSpace πΈ] [inst_4 : CharZero π] {x : πΈ},
x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius β
HasStrictFDerivAt (NormedSpace.exp π) (NormedSpace.exp π x β’ 1) x
The theorem `hasStrictFDerivAt_exp_of_mem_ball` states that for a commutative Banach algebra `πΈ` over a nontrivially normed field `π` of characteristic zero, the exponential map has a strict FrΓ©chet derivative at any point `x` within the disk of convergence. Specifically, the derivative is given by the exponential of `x` times the identity map. The disk of convergence is defined using the radius of the exponential series associated with the normed space.
More concisely: For any commutative Banach algebra over a nontrivially normed field of characteristic zero, the exponential map has a strict FrΓ©chet derivative equal to the identity map at any point in the disk of convergence.
|
hasStrictFDerivAt_exp_zero_of_radius_pos
theorem hasStrictFDerivAt_exp_zero_of_radius_pos :
β {π : Type u_1} {πΈ : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedRing πΈ]
[inst_2 : NormedAlgebra π πΈ] [inst_3 : CompleteSpace πΈ],
0 < (NormedSpace.expSeries π πΈ).radius β HasStrictFDerivAt (NormedSpace.exp π) 1 0
The theorem `hasStrictFDerivAt_exp_zero_of_radius_pos` states that, given a Banach algebra `πΈ` over a normed field `π`, if the exponential series converges on a neighborhood of zero, then the exponential function has a strict FrΓ©chet derivative of `1` at zero. This strict FrΓ©chet derivative is a linear map from `πΈ` to `πΈ` over the field `π`. The convergence of the series is captured by the condition that the radius of convergence of the exponential series is greater than zero.
More concisely: If a Banach algebra over a normed field has an exponential series that converges in a neighborhood of zero, then the exponential function has a strict FrΓ©chet derivative of 1 at zero.
|
hasFDerivAt_exp_of_mem_ball
theorem hasFDerivAt_exp_of_mem_ball :
β {π : Type u_1} {πΈ : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedCommRing πΈ]
[inst_2 : NormedAlgebra π πΈ] [inst_3 : CompleteSpace πΈ] [inst_4 : CharZero π] {x : πΈ},
x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius β
HasFDerivAt (NormedSpace.exp π) (NormedSpace.exp π x β’ 1) x
The theorem `hasFDerivAt_exp_of_mem_ball` states that, for any point `x` in the disk of convergence, the exponential map in a commutative Banach algebra `πΈ` over a normed field `π` of characteristic zero has a FrΓ©chet derivative. More specifically, this derivative is given by the function `exp π x β’ 1 : πΈ βL[π] πΈ`. The disk of convergence is defined by `x` being an element of the set `EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius`. The algebra `πΈ` is required to be a complete space.
More concisely: In a complete commutative Banach algebra over a normed field of characteristic zero, the exponential map at any point in the disk of convergence has a FrΓ©chet derivative given by the function `exp β’ 1 : πΈ βL[π] πΈ`.
|
hasDerivAt_exp_of_mem_ball
theorem hasDerivAt_exp_of_mem_ball :
β {π : Type u_1} [inst : NontriviallyNormedField π] [inst_1 : CompleteSpace π] [inst_2 : CharZero π] {x : π},
x β EMetric.ball 0 (NormedSpace.expSeries π π).radius β HasDerivAt (NormedSpace.exp π) (NormedSpace.exp π x) x
This theorem states that in any complete normed field `π` of characteristic zero, the derivative of the exponential map at any point `x` in the disk of convergence is the exponential map evaluated at `x`. In particular, if `x` lies in the equivalent metric space (eMetric) ball which is centered at 0 with radius being the radius of convergence of the exponential series, then the derivative of the exponential map at point `x` exists and equals `exp π x`.
More concisely: In a complete normed field of characteristic zero, the derivative of the exponential map at any point in the disk of convergence equals the exponential map evaluated at that point.
|
hasStrictFDerivAt_exp
theorem hasStrictFDerivAt_exp :
β {π : Type u_1} {πΈ : Type u_2} [inst : RCLike π] [inst_1 : NormedCommRing πΈ] [inst_2 : NormedAlgebra π πΈ]
[inst_3 : CompleteSpace πΈ] {x : πΈ}, HasStrictFDerivAt (NormedSpace.exp π) (NormedSpace.exp π x β’ 1) x
This theorem states that for any point `x` in a commutative Banach algebra `πΈ` over a scalar field `π` (where `π` can be either the real numbers `β` or the complex numbers `β`), the exponential map has a strict FrΓ©chet derivative at `x`. The derivative is given by the expression `exp π x β’ 1`, acting as a continuous linear map from `πΈ` to itself. The space `πΈ` is assumed to be complete.
More concisely: In a commutative Banach algebra over the real or complex numbers, the exponential map has a strict FrΓ©chet derivative at any point, which is given by the expression `exp(x) β’ 1` as a continuous linear map.
|
hasDerivAt_exp_zero
theorem hasDerivAt_exp_zero : β {π : Type u_1} [inst : RCLike π], HasDerivAt (NormedSpace.exp π) 1 0
The theorem `hasDerivAt_exp_zero` asserts that the derivative of the exponential map, where the exponential map is defined over the real numbers `β` or complex numbers `β`, is `1` at the point `0`. This means that if we consider the exponential function in the context of either real or complex numbers, and examine its rate of change at the point `0`, this rate of change is precisely `1`.
More concisely: The exponential function's derivative at 0 is equal to 1 for both real and complex numbers.
|
hasFDerivAt_exp_zero_of_radius_pos
theorem hasFDerivAt_exp_zero_of_radius_pos :
β {π : Type u_1} {πΈ : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedRing πΈ]
[inst_2 : NormedAlgebra π πΈ] [inst_3 : CompleteSpace πΈ],
0 < (NormedSpace.expSeries π πΈ).radius β HasFDerivAt (NormedSpace.exp π) 1 0
The theorem `hasFDerivAt_exp_zero_of_radius_pos` states that the exponential function in a Banach algebra `πΈ` over a normed field `π` has the FrΓ©chet derivative equal to `1` at zero, given that the exponential function converges on a neighborhood of zero. This holds true for any normed field `π` and Banach algebra `πΈ` that is a normed ring, a normed algebra over `π`, and a complete space, as long as the radius of convergence of the exponential series is greater than zero.
More concisely: Given a Banach algebra over a normed field that is a normed ring, a normed algebra over the field, and complete, with the exponential function converging on a neighborhood of zero and having a positive radius of convergence, the exponential function has a FrΓ©chet derivative equal to 1 at zero.
|
hasFDerivAt_exp
theorem hasFDerivAt_exp :
β {π : Type u_1} {πΈ : Type u_2} [inst : RCLike π] [inst_1 : NormedCommRing πΈ] [inst_2 : NormedAlgebra π πΈ]
[inst_3 : CompleteSpace πΈ] {x : πΈ}, HasFDerivAt (NormedSpace.exp π) (NormedSpace.exp π x β’ 1) x
The theorem states that for any point `x` in a Banach algebra `πΈ` over `π`, where `π` is either the real numbers `β` or the complex numbers `β`, the FrΓ©chet derivative of the exponential map is given by `exp π x β’ 1 : πΈ βL[π] πΈ`. The exponential map is a function that maps any value to its base raised to the power of that value. In this context, the derivative is a measure of how this mapping changes with `x`, and is represented as a continuous linear map from `πΈ` to `πΈ`. The theorem is applicable in the context of a commutative Banach algebra, which is a complete normed vector space that allows for the multiplication of its elements.
More concisely: In a commutative Banach algebra over the real or complex numbers, the FrΓ©chet derivative of the exponential map at any point is a continuous linear map from the algebra to the algebra's bidual.
|
hasStrictFDerivAt_exp_zero
theorem hasStrictFDerivAt_exp_zero :
β {π : Type u_1} {πΈ : Type u_2} [inst : RCLike π] [inst_1 : NormedRing πΈ] [inst_2 : NormedAlgebra π πΈ]
[inst_3 : CompleteSpace πΈ], HasStrictFDerivAt (NormedSpace.exp π) 1 0
This theorem states that for any Banach algebra `πΈ` over a field `π`, which can be either the real numbers `β` or the complex numbers `β`, the function `exp` (exponential function) has a strict FrΓ©chet derivative of `1` at the point `0`. This property is universal regardless of the specific types of `π` and `πΈ`, as long as `πΈ` is a complete space (a Banach space) and `π` is a field that supports the operations of a normed ring and a normed algebra.
More concisely: For any Banach algebra over a normed field, the exponential function has a strict derivative of 1 at 0.
|
hasStrictDerivAt_exp_of_mem_ball
theorem hasStrictDerivAt_exp_of_mem_ball :
β {π : Type u_1} [inst : NontriviallyNormedField π] [inst_1 : CompleteSpace π] [inst_2 : CharZero π] {x : π},
x β EMetric.ball 0 (NormedSpace.expSeries π π).radius β
HasStrictDerivAt (NormedSpace.exp π) (NormedSpace.exp π x) x
This theorem states that in a complete normed field `π` of characteristic zero, the exponential map `exp π` has the derivative `exp π x` at any point `x` within its disk of convergence. The disk of convergence is defined as the set of all points `x` such that the extended distance from `x` to 0 is less than the radius of the exponential series in the normed space. The strict derivative is defined as the difference between the function values at two points, which can be approximated by the product of the difference between the points and the derivative, plus a term that goes to zero as the points approach each other.
More concisely: In a complete normed field of characteristic zero, the exponential map has a derivative equal to its value at any point within its radius of convergence.
|
hasFDerivAt_exp_zero
theorem hasFDerivAt_exp_zero :
β {π : Type u_1} {πΈ : Type u_2} [inst : RCLike π] [inst_1 : NormedRing πΈ] [inst_2 : NormedAlgebra π πΈ]
[inst_3 : CompleteSpace πΈ], HasFDerivAt (NormedSpace.exp π) 1 0
The theorem `hasFDerivAt_exp_zero` states that for any type `π` that behaves like real or complex numbers, and any normed ring `πΈ` that is also a normed algebra over `π` and a complete space, the exponential function in the Banach algebra `πΈ` has a FrΓ©chet derivative of `1` at `0`. In other words, as `x` approaches `0` in the algebra `πΈ`, the difference between `exp(x)` and `1 * x`, divided by the norm of `x`, tends to `0`.
More concisely: For any normed ring `πΈ` that is an algebra over a type `π` behaving like real or complex numbers, and a complete normed space, the exponential function in `πΈ` has a FrΓ©chet derivative of `1` at `0`.
|
hasStrictDerivAt_exp_zero_of_radius_pos
theorem hasStrictDerivAt_exp_zero_of_radius_pos :
β {π : Type u_1} [inst : NontriviallyNormedField π] [inst_1 : CompleteSpace π],
0 < (NormedSpace.expSeries π π).radius β HasStrictDerivAt (NormedSpace.exp π) 1 0
The theorem `hasStrictDerivAt_exp_zero_of_radius_pos` states that for any complete normed field `π` of characteristic zero, if the radius of convergence of the exponential series is positive, then the exponential function has a strict derivative of `1` at zero. In mathematical terms, if the sequence of terms `(xα΅’) : πΈβΏ β¦ (1/n! : π) β’ β xα΅’` converges in a neighborhood around `0`, then the derivative of the exponential function at `0` is `1`, in the sense of strict differentiability, meaning that `f y - f z = (y - z) β’ f' + o(y - z)` as `y, z β x`.
More concisely: If the radius of convergence of the exponential series in a complete normed field of characteristic zero is positive, then the exponential function has strict derivative 1 at 0.
|
hasStrictDerivAt_exp_zero
theorem hasStrictDerivAt_exp_zero : β {π : Type u_1} [inst : RCLike π], HasStrictDerivAt (NormedSpace.exp π) 1 0 := by
sorry
The theorem `hasStrictDerivAt_exp_zero` states that, for any `π` that resembles real or complex numbers, the exponential map has a strict derivative of `1` at the point `0`. In other words, if `π` is either the real numbers `β` or the complex numbers `β`, then the difference between the exponential function values at two points close to `0` is approximately the difference between those two points plus an infinitesimally small error term. This difference becomes exactly equal to the difference between the two points as they both approach zero, demonstrating the definition of the derivative being `1` at `0`.
More concisely: If `π` is either the real numbers `β` or the complex numbers `β`, then the exponential function `exp` on `π` has a strict derivative of `1` at `0`, i.e., `exp' 0 = lim_(hβ0) (exp h - (h + 1))/h = 1`.
|
hasDerivAt_exp
theorem hasDerivAt_exp :
β {π : Type u_1} [inst : RCLike π] {x : π}, HasDerivAt (NormedSpace.exp π) (NormedSpace.exp π x) x
The theorem `hasDerivAt_exp` states that, for any point `x` in a field `π` that behaves like the Real or Complex numbers (denoted as `β` or `β`), the derivative of the exponential function at that point `x` is equal to the value of the exponential function itself at `x` i.e., `exp π x`. In other words, the derivative of `exp π` at any given point is just `exp π` evaluated at that point. This is a well-known property of the exponential function for both real and complex numbers.
More concisely: The derivative of the exponential function equals the exponential function itself at any point in a field behaving like the real or complex numbers.
|
hasStrictDerivAt_exp
theorem hasStrictDerivAt_exp :
β {π : Type u_1} [inst : RCLike π] {x : π}, HasStrictDerivAt (NormedSpace.exp π) (NormedSpace.exp π x) x
The theorem `hasStrictDerivAt_exp` states that the exponential map in either the real numbers `β` or complex numbers `β`, denoted as `π`, has a strict derivative `exp π x` at any point `x`. In other words, for any point `x` in `π`, the change in the exponential function (the derivative) is given by the exponential of `x` itself. This is a property of the exponential function in both real and complex number spaces, and this theorem proves it strictly, i.e., with exact equality rather than as a limit.
More concisely: The exponential function in both real and complex numbers has a strict derivative equal to the function itself at any point.
|
hasDerivAt_exp_zero_of_radius_pos
theorem hasDerivAt_exp_zero_of_radius_pos :
β {π : Type u_1} [inst : NontriviallyNormedField π] [inst_1 : CompleteSpace π],
0 < (NormedSpace.expSeries π π).radius β HasDerivAt (NormedSpace.exp π) 1 0
The theorem `hasDerivAt_exp_zero_of_radius_pos` states that the derivative of the exponential map in a complete normed field `π` of characteristic zero is `1` at the point `0`, provided that the expansion of the exponential map as a formal multilinear series converges on a neighborhood of `0`. In more mathematical terms, if the radius of convergence of the multilinear series expansion of the exponential map is greater than `0`, then the derivative of the exponential map at `0` is `1`. This mirrors the familiar property of the exponential function in real and complex analysis.
More concisely: If the exponential map in a complete normed field of characteristic zero has a multilinear series expansion that converges in a neighborhood of 0, then its derivative at 0 is equal to 1.
|