NormedSpace.expSeries_apply_eq
theorem NormedSpace.expSeries_apply_eq :
β {π : Type u_1} {πΈ : Type u_2} [inst : Field π] [inst_1 : Ring πΈ] [inst_2 : Algebra π πΈ]
[inst_3 : TopologicalSpace πΈ] [inst_4 : TopologicalRing πΈ] (x : πΈ) (n : β),
((NormedSpace.expSeries π πΈ n) fun x_1 => x) = (βn.factorial)β»ΒΉ β’ x ^ n
The theorem `NormedSpace.expSeries_apply_eq` states that for any field `π`, ring `πΈ` with `πΈ` being an algebra over `π`, a topological space and a topological ring, then for any element `x` of `πΈ` and natural number `n`, the `n`-th term of the exponential series at `x` equals to the reciprocal of the factorial of `n` times `x` raised to the power `n`.
More concisely: For any field π, topological space, and topological ring πΈ being an algebra over π, the `n`-th term of the exponential series of an element `x` in πΈ equals to `(1/n!) * x^n`.
|
NormedSpace.star_exp
theorem NormedSpace.star_exp :
β {π : Type u_1} {πΈ : Type u_2} [inst : Field π] [inst_1 : Ring πΈ] [inst_2 : Algebra π πΈ]
[inst_3 : TopologicalSpace πΈ] [inst_4 : TopologicalRing πΈ] [inst_5 : T2Space πΈ] [inst_6 : StarRing πΈ]
[inst_7 : ContinuousStar πΈ] (x : πΈ), star (NormedSpace.exp π x) = NormedSpace.exp π (star x)
This theorem, `NormedSpace.star_exp`, states that for any two types, `π` and `πΈ`, where `π` is a field, `πΈ` is a ring, `πΈ` is an algebra over `π`, `πΈ` has a star operation (that is, it is a star ring), and `πΈ` has a topology that makes it a topological space, a topological ring, and it is Hausdorff (T2 space), and the star operation is continuous (ContinuousStar πΈ), then the star of the exponential function `NormedSpace.exp π x` is equal to the exponential function of the star of `x`, `NormedSpace.exp π (star x)`. This essentially means that the star operation commutes with the exponential function in this normed space context.
More concisely: If `π` is a field, `πΈ` is a commutative topological Hausdorff star ring over `π`, `πΈ` has a topology making it a normed space, and the star operation is continuous, then the star of the exponential function is equal to the exponential function of the star of any element in `πΈ`.
|
NormedSpace.exp_add_of_commute
theorem NormedSpace.exp_add_of_commute :
β {π : Type u_1} {πΈ : Type u_2} [inst : RCLike π] [inst_1 : NormedRing πΈ] [inst_2 : NormedAlgebra π πΈ]
[inst_3 : CompleteSpace πΈ] {x y : πΈ},
Commute x y β NormedSpace.exp π (x + y) = NormedSpace.exp π x * NormedSpace.exp π y
The theorem states that in a Banach-algebra `πΈ` over a field `π` (which can be either the real numbers `β` or the complex numbers `β`), if two elements `x` and `y` commute (i.e., `x * y = y * x`), then the exponential of the sum of `x` and `y` (denoted as `exp π (x + y)`) is equal to the product of the exponentials of `x` and `y` (denoted as `exp π x * exp π y`). This theorem essentially states a specific property of exponentials in the context of Banach algebras with commuting elements.
More concisely: In a Banach algebra over a field, if two commuting elements have exponentially-valued functions, then their sum's exponential is equal to the product of their individual exponentials.
|
NormedSpace.expSeries_hasSum_exp_of_mem_ball
theorem NormedSpace.expSeries_hasSum_exp_of_mem_ball :
β {π : Type u_1} {πΈ : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedRing πΈ]
[inst_2 : NormedAlgebra π πΈ] [inst_3 : CompleteSpace πΈ],
β x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius,
HasSum (fun n => (NormedSpace.expSeries π πΈ n) fun x_1 => x) (NormedSpace.exp π x)
This theorem states that for any non-trivially normed field `π` and a normed ring `πΈ` which is also a normed algebra over `π` and a complete space, for any element `x` that belongs to the `EMetric` ball centered at `0` with radius equal to the radius of the exponential series for `π` and `πΈ`, the series consisting of the `n`-th term of the exponential series applied to `x` converges to the exponential of `π` and `x`. In mathematical terms, if we consider the series β (1/n!) β xα΅’, where xα΅’ are the components of `x`, the sum of this series is exp(π, x), where exp is the exponential function.
More concisely: For any non-trivially normed field `π`, normed ring `πΈ` over `π`, and `x` in the `EMetric` ball of `πΈ` with radius equal to the exponential series' radius, the exponential series β (1/n!) β (π.exp xα΅’) converges to `π.exp x`, where `exp` is the exponential function.
|
NormedSpace.norm_expSeries_summable_of_mem_ball
theorem NormedSpace.norm_expSeries_summable_of_mem_ball :
β {π : Type u_1} {πΈ : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedRing πΈ]
[inst_2 : NormedAlgebra π πΈ],
β x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius,
Summable fun n => β(NormedSpace.expSeries π πΈ n) fun x_1 => xβ
The theorem states that for any nontrivially normed field `π` and any normed ring `πΈ` that is also a normed algebra over `π`, if a point `x` lies within the ball centered at 0 with radius equal to the radius of convergence of the exponential series of `π` and `πΈ`, then the series formed by taking the norm of the `n`-th term of the exponential series evaluated at `x` is summable. In other words, there exists a real number to which the infinite series converges. This theorem links the concept of an exponential series in a normed algebra, the metric space notion of a ball, and the property of a series being summable.
More concisely: For any nontrivially normed field `π` and normed ring `πΈ` that is also a normed algebra over `π`, if an element `x` lies within the ball of radius equal to the radius of convergence of the exponential series in `πΈ` around 0, then the series of the norms of the `n`-th term of the exponential series evaluated at `x` is convergent.
|
NormedSpace.expSeries_radius_eq_top
theorem NormedSpace.expSeries_radius_eq_top :
β (π : Type u_1) (πΈ : Type u_2) [inst : RCLike π] [inst_1 : NormedRing πΈ] [inst_2 : NormedAlgebra π πΈ],
(NormedSpace.expSeries π πΈ).radius = β€
The theorem `NormedSpace.expSeries_radius_eq_top` states that in a normed algebra `πΈ` over a field `π`, which is either the real numbers β or the complex numbers β, the series that defines the exponential map has an infinite radius of convergence. In other words, the series converges for all inputs in the algebra `πΈ`.
More concisely: In a normed algebra over a field, the exponential series has infinite radius of convergence.
|
NormedSpace.exp_add_of_mem_ball
theorem NormedSpace.exp_add_of_mem_ball :
β {π : Type u_1} {πΈ : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedCommRing πΈ]
[inst_2 : NormedAlgebra π πΈ] [inst_3 : CompleteSpace πΈ] [inst_4 : CharZero π] {x y : πΈ},
x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius β
y β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius β
NormedSpace.exp π (x + y) = NormedSpace.exp π x * NormedSpace.exp π y
The theorem `NormedSpace.exp_add_of_mem_ball` states that in a commutative Banach-algebra `πΈ` over a normed field `π` of characteristic zero, the exponential of the sum of two elements `x` and `y` is equal to the product of the exponentials of the two elements. This property holds for all `x` and `y` that are in the disk of convergence, which is defined as the set of all points that are within a certain distance (the radius of the `expSeries` for `π` and `πΈ`) from the origin. The exponential function is defined using the `expSeries`, a formal multilinear series where the n-th term is a continuous multilinear map scaled by the reciprocal of n factorial.
More concisely: In a commutative Banach algebra over a normed field of characteristic zero, the exponent of the sum of two elements in the disk of convergence equals the product of their exponentials.
|
NormedSpace.expSeries_radius_pos
theorem NormedSpace.expSeries_radius_pos :
β (π : Type u_1) (πΈ : Type u_2) [inst : RCLike π] [inst_1 : NormedRing πΈ] [inst_2 : NormedAlgebra π πΈ],
0 < (NormedSpace.expSeries π πΈ).radius
The theorem `NormedSpace.expSeries_radius_pos` asserts that for any types `π` and `πΈ` where `π` is a type that behaves like real-complex numbers (as expressed by `[inst : RCLike π]`), and `πΈ` is a normed ring and a normed algebra over `π` (as expressed by `[inst_1 : NormedRing πΈ]` and `[inst_2 : NormedAlgebra π πΈ]`), the radius of convergence of the formal multilinear series `NormedSpace.expSeries π πΈ` (which defines the exponential series for a multilinear map on `πΈ`) is strictly positive. In mathematical terms, it ensures that the exponential series converges within a non-zero radius around any point in the normed space `πΈ`.
More concisely: The radius of convergence of the exponential series for a multilinear map on a normed algebra over a type behaving like real or complex numbers is strictly positive.
|
NormedSpace.map_exp_of_mem_ball
theorem NormedSpace.map_exp_of_mem_ball :
β {π : Type u_1} {πΈ : Type u_2} {πΉ : Type u_3} [inst : NontriviallyNormedField π] [inst_1 : NormedRing πΈ]
[inst_2 : NormedRing πΉ] [inst_3 : NormedAlgebra π πΈ] [inst_4 : NormedAlgebra π πΉ] [inst_5 : CompleteSpace πΈ]
{F : Type u_4} [inst_6 : FunLike F πΈ πΉ] [inst_7 : RingHomClass F πΈ πΉ] (f : F),
Continuous βf β
β x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius, f (NormedSpace.exp π x) = NormedSpace.exp π (f x)
This theorem states that for any continuous ring homomorphism `f`, it commutes with the exponential function. More specifically, given a nontrivially normed field `π` and normed rings `πΈ` and `πΉ` with `πΈ` being a complete space, and assuming that terms of type `F` have an injective coercion to functions from `πΈ` to `πΉ` and that `F` is a ring homomorphism class, if `f` is a continuous map then for any `x` in the open ball centered at `0` with radius given by the radius of the exponential formal multilinear series, we have `f(exp(π, x)) = exp(π, f(x))`. In other words, applying `f` to the exponential of `x` is the same as taking the exponential of `f(x)`.
More concisely: Given a continuous ring homomorphism `f` between complete, normed rings `πΈ` and `πΉ` over a nontrivially normed field `π`, and assuming `F` is a ring homomorphism class with injective coercion from terms of type `F` to functions `πΈ β πΉ`, then `f(exp(x)) = exp(f(x))` for all `x` in the open ball of `πΈ` centered at `0` with radius equal to the exponential series' radius.
|
NormedSpace.of_real_exp_β_β
theorem NormedSpace.of_real_exp_β_β : β (r : β), β(NormedSpace.exp β r) = NormedSpace.exp β βr
This theorem states that for every real number `r`, the normed space exponential function applied to `r` (when viewed as a real number) equals the normed space exponential function applied to `r` (when viewed as a complex number). This is similar to the `Complex.ofReal_exp` theorem, but using `NormedSpace.exp` instead of `Complex.exp`. In mathematical notation, it would be expressed as β r β β, exp_β(r) = exp_β(r), where exp_β and exp_β denote the exponential function in the real and complex normed spaces respectively.
More concisely: For every real number `r`, the normed space exponential function applied to `r` as a real number equals the normed space exponential function applied to the complex number `r` obtained by its conversion from a real number.
|
NormedSpace.exp_units_conj
theorem NormedSpace.exp_units_conj :
β (π : Type u_1) {πΈ : Type u_2} [inst : RCLike π] [inst_1 : NormedRing πΈ] [inst_2 : NormedAlgebra π πΈ]
[inst_3 : CompleteSpace πΈ] (y : πΈΛ£) (x : πΈ),
NormedSpace.exp π (βy * x * βyβ»ΒΉ) = βy * NormedSpace.exp π x * βyβ»ΒΉ
This theorem states that for any type `π` that behaves like a real/closed field (RCLike), a type `πΈ` that forms a normed ring, and for `πΈ` as a normed algebra over `π` in a complete space, the exponential function (`NormedSpace.exp`) applied to a value `x` of type `πΈ`, multiplied on the left by a unit `y` and on the right by the inverse of the same unit `y`, is equivalent to the exponential of `x` itself, again multiplied on the left by `y` and on the right by `y`'s inverse. In mathematical terms, it asserts that `exp(π, y * x * yβ»ΒΉ) = y * exp(π, x) * yβ»ΒΉ` for all `x` in `πΈ` and unit `y` in `πΈΛ£`.
More concisely: For any RCLike field `π`, normed ring `πΈ`, and unit `y` in `πΈ`, the exponential function applied to `x` in `πΈ` satisfies `exp(π, y * x * yβ»ΒΉ) = y * exp(π, x) * yβ»ΒΉ`.
|
NormedSpace.exp_add_of_commute_of_mem_ball
theorem NormedSpace.exp_add_of_commute_of_mem_ball :
β {π : Type u_1} {πΈ : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedRing πΈ]
[inst_2 : NormedAlgebra π πΈ] [inst_3 : CompleteSpace πΈ] [inst_4 : CharZero π] {x y : πΈ},
Commute x y β
x β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius β
y β EMetric.ball 0 (NormedSpace.expSeries π πΈ).radius β
NormedSpace.exp π (x + y) = NormedSpace.exp π x * NormedSpace.exp π y
The theorem `NormedSpace.exp_add_of_commute_of_mem_ball` states that in a Banach algebra πΈ over a normed field π of characteristic zero, if two elements `x` and `y` commute (i.e., `x * y = y * x`) and both belong to the disc of convergence (i.e., the set of all points `z` for which the Euclidean distance from `z` to the origin is less than the radius of convergence of the exponential series), then the exponential of their sum is equal to the product of their exponentials. In other words, `exp π (x + y) = (exp π x) * (exp π y)`.
More concisely: In a Banach algebra over a characteristic zero normed field, if two commuting elements belong to the disc of convergence, then their exponentials commute and their product is the exponential of their sum.
|
NormedSpace.exp_zero
theorem NormedSpace.exp_zero :
β {π : Type u_1} {πΈ : Type u_2} [inst : Field π] [inst_1 : Ring πΈ] [inst_2 : Algebra π πΈ]
[inst_3 : TopologicalSpace πΈ] [inst_4 : TopologicalRing πΈ], NormedSpace.exp π 0 = 1
The theorem `NormedSpace.exp_zero` states that for any given types `π` and `πΈ`, where `π` is a field, `πΈ` is a ring and `πΈ` is an algebra over `π`, if `πΈ` is also a topological space and a topological ring, then the exponential of zero in this normed space is equal to one. In mathematical terms, for such structures, we have `exp(0) = 1`.
More concisely: For a normed space `πΈ` over a field `π`, where `πΈ` is a ring, an algebra over `π`, a topological space, and a topological ring, the exponential function in `πΈ` evaluates to one at zero, i.e., `exp(0) = 1`.
|
NormedSpace.expSeries_eq_expSeries
theorem NormedSpace.expSeries_eq_expSeries :
β (π : Type u_1) (π' : Type u_2) (πΈ : Type u_3) [inst : Field π] [inst_1 : Field π'] [inst_2 : Ring πΈ]
[inst_3 : Algebra π πΈ] [inst_4 : Algebra π' πΈ] [inst_5 : TopologicalSpace πΈ] [inst_6 : TopologicalRing πΈ] (n : β)
(x : πΈ), ((NormedSpace.expSeries π πΈ n) fun x_1 => x) = (NormedSpace.expSeries π' πΈ n) fun x_1 => x
The theorem `NormedSpace.expSeries_eq_expSeries` states that if a normed ring `πΈ` is a normed algebra over two fields `π` and `π'`, then the exponential series `expSeries` defined on `πΈ` with respect to each of these fields `π` and `π'` is identical. Specifically, for any natural number `n` and any element `x` in `πΈ`, the `n`-th term of the `expSeries` computed with respect to the field `π` applied to `x` is equal to the `n`-th term of the `expSeries` computed with respect to the field `π'` applied to `x`.
More concisely: For any normed ring `πΈ` over fields `π` and `π'`, and for all natural numbers `n` and elements `x` in `πΈ`, the `n`-th terms of the exponential series of `x` with respect to `π` and `π'` are equal.
|
NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos
theorem NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos :
β {π : Type u_1} {πΈ : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedRing πΈ]
[inst_2 : NormedAlgebra π πΈ] [inst_3 : CompleteSpace πΈ],
0 < (NormedSpace.expSeries π πΈ).radius β
HasFPowerSeriesOnBall (NormedSpace.exp π) (NormedSpace.expSeries π πΈ) 0 (NormedSpace.expSeries π πΈ).radius
The theorem `NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos` states that for any field `π` which is a non-trivially normed field, and any type `πΈ` which is a normed ring over `π`, and a normed algebra over `π`, and is a complete space, if the radius of the exponential series `NormedSpace.expSeries π πΈ` is positive, then the exponential function `NormedSpace.exp π` has an `F` power series on a ball centered at the origin with the same radius as that of the exponential series. Here, an `F` power series refers to a formal power series, and the ball refers to a set of points in `πΈ` within a certain distance from the origin.
More concisely: For any complete, normed algebra `πΈ` over a non-trivially normed field `π`, if the radius of convergence of the exponential series of `πΈ` is positive, then the exponential function has an `F` power series expansion that converges on the open ball of radius equal to the series's convergence radius.
|
NormedSpace.exp_sum
theorem NormedSpace.exp_sum :
β {π : Type u_1} {πΈ : Type u_2} [inst : RCLike π] [inst_1 : NormedCommRing πΈ] [inst_2 : NormedAlgebra π πΈ]
[inst_3 : CompleteSpace πΈ] {ΞΉ : Type u_3} (s : Finset ΞΉ) (f : ΞΉ β πΈ),
NormedSpace.exp π (s.sum fun i => f i) = s.prod fun i => NormedSpace.exp π (f i)
This theorem states that, in a commutative Banach-algebra over a ring-like structure, the exponential of the sum of a set of elements, computed with respect to the normed space, is equal to the product of the exponentials of each element in the set. More formally, for any given types π and πΈ, where π is a ring-like structure and πΈ is a complete commutative normed ring that is also a normed algebra over π, and for any finite set `s` of type `ΞΉ` and a function `f` from `ΞΉ` to πΈ, the exponential of the sum of `f(i)` for all `i` in `s` is the same as the product of the exponential of `f(i)` for all `i` in `s`.
More concisely: In a commutative Banach-algebra over a ring-like structure where the base ring is a complete commutative normed ring, the exponential of the sum of a finite set of elements is equal to the product of the exponentials of each element for that normed algebra.
|
NormedSpace.exp_eq_tsum
theorem NormedSpace.exp_eq_tsum :
β {π : Type u_1} {πΈ : Type u_2} [inst : Field π] [inst_1 : Ring πΈ] [inst_2 : Algebra π πΈ]
[inst_3 : TopologicalSpace πΈ] [inst_4 : TopologicalRing πΈ],
NormedSpace.exp π = fun x => β' (n : β), (βn.factorial)β»ΒΉ β’ x ^ n
The theorem `NormedSpace.exp_eq_tsum` states that for any two types `π` and `πΈ`, where `π` is a field, `πΈ` is a ring, `πΈ` is an algebra over `π`, `πΈ` has a topological structure, and the ring operations in `πΈ` are continuous (`πΈ` is a topological ring), the exponential function in the normed space over `π` is equal to the infinite sum (`tsum`) of the terms `(β(Nat.factorial n))β»ΒΉ β’ x ^ n` for all natural numbers `n`. Here, `β(Nat.factorial n))β»ΒΉ` is the inverse of the factorial of `n`, `β’` is the scalar multiplication in the algebra, and `x ^ n` is `x` raised to the power `n`.
More concisely: For any field `π`, ring `πΈ` over `π` that is a topological ring with continuous ring operations, the exponential function in the normed space over `π` equals the infinite sum of the scaled power series of `x` in `πΈ`, where the scale factor is the reciprocal of the factorial for each natural number `n`.
|
NormedSpace.map_exp
theorem NormedSpace.map_exp :
β (π : Type u_1) {πΈ : Type u_2} {πΉ : Type u_3} [inst : RCLike π] [inst_1 : NormedRing πΈ]
[inst_2 : NormedAlgebra π πΈ] [inst_3 : NormedRing πΉ] [inst_4 : NormedAlgebra π πΉ] [inst_5 : CompleteSpace πΈ]
{F : Type u_4} [inst_6 : FunLike F πΈ πΉ] [inst_7 : RingHomClass F πΈ πΉ] (f : F),
Continuous βf β β (x : πΈ), f (NormedSpace.exp π x) = NormedSpace.exp π (f x)
This theorem, named `NormedSpace.map_exp`, states that for any continuous ring homomorphism `f`, the operation of `f` commutes with the exponential function in the context of normed spaces. More specifically, given a type `π` and types `πΈ` and `πΉ` such that they form normed rings and normed algebras over `π`, and `πΈ` is a complete space, along with a type `F` that acts as a function from `πΈ` to `πΉ` and forms a ring homomorphism, for any `x` in `πΈ`, applying `f` to the exponential of `x` is the same as taking the exponential of `f(x)`. The continuity of `f` is a necessary condition for this property.
More concisely: Given a complete normed ring and algebra πΈ over a ring π, a continuous ring homomorphism F : πΈ -> πΉ between them, and x in πΈ, then F(exp(x)) = exp(F(x)).
|
NormedSpace.expSeries_sum_eq
theorem NormedSpace.expSeries_sum_eq :
β {π : Type u_1} {πΈ : Type u_2} [inst : Field π] [inst_1 : Ring πΈ] [inst_2 : Algebra π πΈ]
[inst_3 : TopologicalSpace πΈ] [inst_4 : TopologicalRing πΈ] (x : πΈ),
(NormedSpace.expSeries π πΈ).sum x = β' (n : β), (βn.factorial)β»ΒΉ β’ x ^ n
The theorem `NormedSpace.expSeries_sum_eq` states that for any types `π` of a field and `πΈ` of a ring, with `πΈ` being a `π`-algebra and both `π` and `πΈ` being topological rings, the sum of the exponential series on a given element `x` from `πΈ` equals the sum of the series formed by the term `(1/n!) * x^n` for all natural numbers `n`. Here, `n!` denotes the factorial of `n` and `x^n` denotes `x` raised to the power `n`.
More concisely: For any field `π`, ring `πΈ` that is a `π`-algebra and topological ring, the exponential series of an element `x` in `πΈ` equals the sum of the series of `(1/n!) * x^n` for all natural numbers `n`.
|
NormedSpace.exp_sum_of_commute
theorem NormedSpace.exp_sum_of_commute :
β {π : Type u_1} {πΈ : Type u_2} [inst : RCLike π] [inst_1 : NormedRing πΈ] [inst_2 : NormedAlgebra π πΈ]
[inst_3 : CompleteSpace πΈ] {ΞΉ : Type u_4} (s : Finset ΞΉ) (f : ΞΉ β πΈ)
(h : (βs).Pairwise fun i j => Commute (f i) (f j)),
NormedSpace.exp π (s.sum fun i => f i) = s.noncommProd (fun i => NormedSpace.exp π (f i)) β―
The theorem `NormedSpace.exp_sum_of_commute` states that in a Banach algebra `πΈ` over either the real numbers `β` or the complex numbers `β`, if you have a family of elements `f i` that mutually commute (meaning the multiplication operation for any two of these elements commutes), then the exponential function of the sum of these elements, `exp π (β i, f i)`, equals the product of the exponential function of each individual element, `β i, exp π (f i)`. This holds true not just for any subset of elements, but specifically for a finite set `s` of such elements.
More concisely: In a Banach algebra over the real or complex numbers, if a finite set of commuting elements has exponentials defined, then the exponential of their sum equals the product of their individual exponentials.
|
NormedSpace.exp_eq_exp
theorem NormedSpace.exp_eq_exp :
β (π : Type u_1) (π' : Type u_2) (πΈ : Type u_3) [inst : Field π] [inst_1 : Field π'] [inst_2 : Ring πΈ]
[inst_3 : Algebra π πΈ] [inst_4 : Algebra π' πΈ] [inst_5 : TopologicalSpace πΈ] [inst_6 : TopologicalRing πΈ],
NormedSpace.exp π = NormedSpace.exp π'
The theorem "NormedSpace.exp_eq_exp" states that if we have a normed ring (let's denote it as `πΈ`), which is also a normed algebra over two different fields (denoted as `π` and `π'`), then the exponential function as defined in the context of these two fields (`π` and `π'`) over `πΈ` are the same. In other words, the choice of field does not change the definition of the exponential function over a normed algebra.
More concisely: For a normed ring `πΈ` that is also a normed algebra over two fields `π` and `π'`, the exponential functions defined over `πΈ` with respect to `π` and `π'` are equal.
|
NormedSpace.exp_add
theorem NormedSpace.exp_add :
β {π : Type u_1} {πΈ : Type u_2} [inst : RCLike π] [inst_1 : NormedCommRing πΈ] [inst_2 : NormedAlgebra π πΈ]
[inst_3 : CompleteSpace πΈ] {x y : πΈ}, NormedSpace.exp π (x + y) = NormedSpace.exp π x * NormedSpace.exp π y
This theorem states that in a commutative Banach algebra `πΈ` over a field `π` (which can be either the real numbers β or the complex numbers β), the exponential function satisfies the property `exp π (x + y) = exp π x * exp π y` for any `x` and `y` in `πΈ`. This is a statement about the exponential function in a normed space, specifically in a Banach algebra, which is a kind of complete normed vector space.
More concisely: In a commutative Banach algebra over a field, the exponential function satisfies the property of being multiplicatively closed, that is, exp(x + y) = exp(x) * exp(y) for all x, y in the algebra.
|