Exponential in a Banach algebra

In this file, we define exp 𝕂 : 𝔸 → 𝔸, the exponential map in a topological algebra 𝔸 over a field 𝕂.

While for most interesting results we need 𝔸 to be normed algebra, we do not require this in the definition in order to make exp independent of a particular choice of norm. The definition also does not require that 𝔸 be complete, but we need to assume it for most results.

We then prove some basic results, but we avoid importing derivatives here to minimize dependencies. Results involving derivatives and comparisons with Real.exp and Complex.exp can be found in Analysis.SpecialFunctions.Exponential.

Main results

We prove most result for an arbitrary field 𝕂, and then specialize to 𝕂 = ℝ or 𝕂 = ℂ.

General case

• exp_add_of_commute_of_mem_ball : if 𝕂 has characteristic zero, then given two commuting elements x and y in the disk of convergence, we have exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)
• exp_add_of_mem_ball : if 𝕂 has characteristic zero and 𝔸 is commutative, then given two elements x and y in the disk of convergence, we have exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)
• exp_neg_of_mem_ball : if 𝕂 has characteristic zero and 𝔸 is a division ring, then given an element x in the disk of convergence, we have exp 𝕂 (-x) = (exp 𝕂 x)⁻¹.

𝕂 = ℝ or 𝕂 = ℂ

• expSeries_radius_eq_top : the FormalMultilinearSeries defining exp 𝕂 has infinite radius of convergence
• exp_add_of_commute : given two commuting elements x and y, we have exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)
• exp_add : if 𝔸 is commutative, then we have exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y) for any x and y
• exp_neg : if 𝔸 is a division ring, then we have exp 𝕂 (-x) = (exp 𝕂 x)⁻¹.
• exp_sum_of_commute : the analogous result to exp_add_of_commute for Finset.sum.
• exp_sum : the analogous result to exp_add for Finset.sum.
• exp_nsmul : repeated addition in the domain corresponds to repeated multiplication in the codomain.
• exp_zsmul : repeated addition in the domain corresponds to repeated multiplication in the codomain.

Other useful compatibility results

• exp_eq_exp : if 𝔸 is a normed algebra over two fields 𝕂 and 𝕂', then exp 𝕂 = exp 𝕂' 𝔸

def expSeries (𝕂 : Type u_1) (𝔸 : Type u_2) [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] : FormalMultilinearSeries 𝕂 𝔸 𝔸

expSeries 𝕂 𝔸 is the FormalMultilinearSeries whose n-th term is the map (xᵢ) : 𝔸ⁿ ↦ (1/n! : 𝕂) • ∏ xᵢ. Its sum is the exponential map exp 𝕂 : 𝔸 → 𝔸.

noncomputable def exp (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (x : 𝔸) : 𝔸

exp 𝕂 : 𝔸 → 𝔸 is the exponential map determined by the action of 𝕂 on 𝔸. It is defined as the sum of the FormalMultilinearSeries expSeries 𝕂 𝔸.

Note that when 𝔸 = Matrix n n 𝕂, this is the Matrix Exponential; see Analysis.NormedSpace.MatrixExponential for lemmas specific to that case.

theorem expSeries_apply_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (x : 𝔸) (n : ℕ) : (↑(expSeries 𝕂 𝔸 n) fun x => x) = (↑(Nat.factorial n))⁻¹ • x ^ n

theorem expSeries_apply_eq' {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (x : 𝔸) : (fun n => ↑(expSeries 𝕂 𝔸 n) fun x => x) = fun n => (↑(Nat.factorial n))⁻¹ • x ^ n

theorem expSeries_sum_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (x : 𝔸) : FormalMultilinearSeries.sum (expSeries 𝕂 𝔸) x = ∑' (n : ℕ), (↑(Nat.factorial n))⁻¹ • x ^ n

theorem exp_eq_tsum {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] : exp 𝕂 = fun x => ∑' (n : ℕ), (↑(Nat.factorial n))⁻¹ • x ^ n

theorem expSeries_apply_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (n : ℕ) : (↑(expSeries 𝕂 𝔸 n) fun x => 0) = Pi.single 0 1 n

@[simp]

theorem exp_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] : exp 𝕂 0 = 1

@[simp]

theorem exp_op {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] (x : 𝔸) : exp 𝕂 (MulOpposite.op x) = MulOpposite.op (exp 𝕂 x)

@[simp]

theorem exp_unop {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] (x : 𝔸ᵐᵒᵖ) : exp 𝕂 (MulOpposite.unop x) = MulOpposite.unop (exp 𝕂 x)

theorem star_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] (x : 𝔸) : star (exp 𝕂 x) = exp 𝕂 (star x)

theorem IsSelfAdjoint.exp (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] {x : 𝔸} (h : IsSelfAdjoint x) : IsSelfAdjoint (exp 𝕂 x)

theorem Commute.exp_right (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] {x : 𝔸} {y : 𝔸} (h : Commute x y) : Commute x (exp 𝕂 y)

theorem Commute.exp_left (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] {x : 𝔸} {y : 𝔸} (h : Commute x y) : Commute (exp 𝕂 x) y

theorem Commute.exp (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] {x : 𝔸} {y : 𝔸} (h : Commute x y) : Commute (exp 𝕂 x) (exp 𝕂 y)

theorem expSeries_apply_eq_div {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [DivisionRing 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (x : 𝔸) (n : ℕ) : (↑(expSeries 𝕂 𝔸 n) fun x => x) = x ^ n / ↑(Nat.factorial n)

theorem expSeries_apply_eq_div' {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [DivisionRing 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (x : 𝔸) : (fun n => ↑(expSeries 𝕂 𝔸 n) fun x => x) = fun n => x ^ n / ↑(Nat.factorial n)

theorem expSeries_sum_eq_div {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [DivisionRing 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (x : 𝔸) : FormalMultilinearSeries.sum (expSeries 𝕂 𝔸) x = ∑' (n : ℕ), x ^ n / ↑(Nat.factorial n)

theorem exp_eq_tsum_div {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [DivisionRing 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] : exp 𝕂 = fun x => ∑' (n : ℕ), x ^ n / ↑(Nat.factorial n)

theorem norm_expSeries_summable_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : Summable fun n => ‖↑(expSeries 𝕂 𝔸 n) fun x => x‖

theorem norm_expSeries_summable_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : Summable fun n => ‖(↑(Nat.factorial n))⁻¹ • x ^ n‖

theorem expSeries_summable_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : Summable fun n => ↑(expSeries 𝕂 𝔸 n) fun x => x

theorem expSeries_summable_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : Summable fun n => (↑(Nat.factorial n))⁻¹ • x ^ n

theorem expSeries_hasSum_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : HasSum (fun n => ↑(expSeries 𝕂 𝔸 n) fun x => x) (exp 𝕂 x)

theorem expSeries_hasSum_exp_of_mem_ball' {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • x ^ n) (exp 𝕂 x)

theorem hasFPowerSeriesOnBall_exp_of_radius_pos {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)) : HasFPowerSeriesOnBall (exp 𝕂) (expSeries 𝕂 𝔸) 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))

theorem hasFPowerSeriesAt_exp_zero_of_radius_pos {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)) : HasFPowerSeriesAt (exp 𝕂) (expSeries 𝕂 𝔸) 0

theorem continuousOn_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] : ContinuousOn (exp 𝕂) (EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)))

theorem analyticAt_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : AnalyticAt 𝕂 (exp 𝕂) x

theorem exp_add_of_commute_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} {y : 𝔸} (hxy : Commute x y) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) (hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y

In a Banach-algebra 𝔸 over a normed field 𝕂 of characteristic zero, if x and y are in the disk of convergence and commute, then exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y).

noncomputable def invertibleExpOfMemBall {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : Invertible (exp 𝕂 x)

exp 𝕂 x has explicit two-sided inverse exp 𝕂 (-x).

theorem isUnit_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : IsUnit (exp 𝕂 x)

theorem invOf_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) [Invertible (exp 𝕂 x)] : ⅟(exp 𝕂 x) = exp 𝕂 (-x)

theorem map_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} {𝔹 : Type u_3} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedRing 𝔹] [NormedAlgebra 𝕂 𝔸] [NormedAlgebra 𝕂 𝔹] [CompleteSpace 𝔸] {F : Type u_4} [RingHomClass F 𝔸 𝔹] (f : F) (hf : Continuous ↑f) (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : ↑f (exp 𝕂 x) = exp 𝕂 (↑f x)

Any continuous ring homomorphism commutes with exp.

theorem algebraMap_exp_comm_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝕂] (x : 𝕂) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝕂))) : ↑(algebraMap 𝕂 𝔸) (exp 𝕂 x) = exp 𝕂 (↑(algebraMap 𝕂 𝔸) x)

theorem norm_expSeries_div_summable_of_mem_ball (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : Summable fun n => ‖x ^ n / ↑(Nat.factorial n)‖

theorem expSeries_div_summable_of_mem_ball (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : Summable fun n => x ^ n / ↑(Nat.factorial n)

theorem expSeries_div_hasSum_exp_of_mem_ball (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : HasSum (fun n => x ^ n / ↑(Nat.factorial n)) (exp 𝕂 x)

theorem exp_neg_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CharZero 𝕂] [CompleteSpace 𝔸] {x : 𝔸} (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : exp 𝕂 (-x) = (exp 𝕂 x)⁻¹

theorem exp_add_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} {y : 𝔸} (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) (hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))) : exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y

In a commutative Banach-algebra 𝔸 over a normed field 𝕂 of characteristic zero, exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y) for all x, y in the disk of convergence.

theorem expSeries_radius_eq_top (𝕂 : Type u_1) (𝔸 : Type u_2) [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] : FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = ⊤

In a normed algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ, the series defining the exponential map has an infinite radius of convergence.

theorem expSeries_radius_pos (𝕂 : Type u_1) (𝔸 : Type u_2) [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)

theorem norm_expSeries_summable {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) : Summable fun n => ‖↑(expSeries 𝕂 𝔸 n) fun x => x‖

theorem norm_expSeries_summable' {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) : Summable fun n => ‖(↑(Nat.factorial n))⁻¹ • x ^ n‖

theorem expSeries_summable {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : Summable fun n => ↑(expSeries 𝕂 𝔸 n) fun x => x

theorem expSeries_summable' {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : Summable fun n => (↑(Nat.factorial n))⁻¹ • x ^ n

theorem expSeries_hasSum_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : HasSum (fun n => ↑(expSeries 𝕂 𝔸 n) fun x => x) (exp 𝕂 x)

theorem exp_series_hasSum_exp' {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : HasSum (fun n => (↑(Nat.factorial n))⁻¹ • x ^ n) (exp 𝕂 x)

theorem exp_hasFPowerSeriesOnBall {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] : HasFPowerSeriesOnBall (exp 𝕂) (expSeries 𝕂 𝔸) 0 ⊤

theorem exp_hasFPowerSeriesAt_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] : HasFPowerSeriesAt (exp 𝕂) (expSeries 𝕂 𝔸) 0

theorem exp_continuous {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] : Continuous (exp 𝕂)

theorem exp_analytic {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : AnalyticAt 𝕂 (exp 𝕂) x

theorem exp_add_of_commute {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {x : 𝔸} {y : 𝔸} (hxy : Commute x y) : exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y

In a Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ, if x and y commute, then exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y).

noncomputable def invertibleExp (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : Invertible (exp 𝕂 x)

exp 𝕂 x has explicit two-sided inverse exp 𝕂 (-x).

theorem isUnit_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : IsUnit (exp 𝕂 x)

theorem invOf_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) [Invertible (exp 𝕂 x)] : ⅟(exp 𝕂 x) = exp 𝕂 (-x)

theorem Ring.inverse_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : Ring.inverse (exp 𝕂 x) = exp 𝕂 (-x)

theorem exp_mem_unitary_of_mem_skewAdjoint (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] {x : 𝔸} (h : x ∈ skewAdjoint 𝔸) : exp 𝕂 x ∈ unitary 𝔸

theorem exp_sum_of_commute {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {ι : Type u_4} (s : Finset ι) (f : ι → 𝔸) (h : Set.Pairwise ↑s fun i j => Commute (f i) (f j)) : exp 𝕂 (Finset.sum s fun i => f i) = Finset.noncommProd s (fun i => exp 𝕂 (f i)) (_ : ∀ (i : ι), i ∈ ↑s → ∀ (j : ι), j ∈ ↑s → i ≠ j → Commute (exp 𝕂 (f i)) (exp 𝕂 (f j)))

In a Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ, if a family of elements f i mutually commute then exp 𝕂 (∑ i, f i) = ∏ i, exp 𝕂 (f i).

theorem exp_nsmul {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (n : ℕ) (x : 𝔸) : exp 𝕂 (n • x) = exp 𝕂 x ^ n

theorem map_exp (𝕂 : Type u_1) {𝔸 : Type u_2} {𝔹 : Type u_3} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [NormedRing 𝔹] [NormedAlgebra 𝕂 𝔹] [CompleteSpace 𝔸] {F : Type u_4} [RingHomClass F 𝔸 𝔹] (f : F) (hf : Continuous ↑f) (x : 𝔸) : ↑f (exp 𝕂 x) = exp 𝕂 (↑f x)

Any continuous ring homomorphism commutes with exp.

theorem exp_smul (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {G : Type u_4} [Monoid G] [MulSemiringAction G 𝔸] [ContinuousConstSMul G 𝔸] (g : G) (x : 𝔸) : exp 𝕂 (g • x) = g • exp 𝕂 x

theorem exp_units_conj (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (y : 𝔸ˣ) (x : 𝔸) : exp 𝕂 (↑y * x * ↑y⁻¹) = ↑y * exp 𝕂 x * ↑y⁻¹

theorem exp_units_conj' (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (y : 𝔸ˣ) (x : 𝔸) : exp 𝕂 (↑y⁻¹ * x * ↑y) = ↑y⁻¹ * exp 𝕂 x * ↑y

@[simp]

theorem Prod.fst_exp (𝕂 : Type u_1) {𝔸 : Type u_2} {𝔹 : Type u_3} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [NormedRing 𝔹] [NormedAlgebra 𝕂 𝔹] [CompleteSpace 𝔸] [CompleteSpace 𝔹] (x : 𝔸 × 𝔹) : (exp 𝕂 x).fst = exp 𝕂 x.fst

@[simp]

theorem Prod.snd_exp (𝕂 : Type u_1) {𝔸 : Type u_2} {𝔹 : Type u_3} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [NormedRing 𝔹] [NormedAlgebra 𝕂 𝔹] [CompleteSpace 𝔸] [CompleteSpace 𝔹] (x : 𝔸 × 𝔹) : (exp 𝕂 x).snd = exp 𝕂 x.snd

@[simp]

theorem Pi.exp_apply (𝕂 : Type u_1) [IsROrC 𝕂] {ι : Type u_4} {𝔸 : ι → Type u_5} [Fintype ι] [(i : ι) → NormedRing (𝔸 i)] [(i : ι) → NormedAlgebra 𝕂 (𝔸 i)] [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i) (i : ι) : exp 𝕂 ((i : ι) → 𝔸 i) NormedField.toField Pi.ring (Pi.algebra ι fun i => 𝔸 i) Pi.topologicalSpace (_ : TopologicalRing ((b : ι) → 𝔸 b)) x i = exp 𝕂 (x i)

theorem Pi.exp_def (𝕂 : Type u_1) [IsROrC 𝕂] {ι : Type u_4} {𝔸 : ι → Type u_5} [Fintype ι] [(i : ι) → NormedRing (𝔸 i)] [(i : ι) → NormedAlgebra 𝕂 (𝔸 i)] [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i) : exp 𝕂 x = fun i => exp 𝕂 (x i)

theorem Function.update_exp (𝕂 : Type u_1) [IsROrC 𝕂] {ι : Type u_4} {𝔸 : ι → Type u_5} [Fintype ι] [DecidableEq ι] [(i : ι) → NormedRing (𝔸 i)] [(i : ι) → NormedAlgebra 𝕂 (𝔸 i)] [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i) (j : ι) (xj : 𝔸 j) : Function.update (exp 𝕂 x) j (exp 𝕂 xj) = exp 𝕂 (Function.update x j xj)

theorem algebraMap_exp_comm {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝕂) : ↑(algebraMap 𝕂 𝔸) (exp 𝕂 x) = exp 𝕂 (↑(algebraMap 𝕂 𝔸) x)

theorem norm_expSeries_div_summable (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) : Summable fun n => ‖x ^ n / ↑(Nat.factorial n)‖

theorem expSeries_div_summable (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : Summable fun n => x ^ n / ↑(Nat.factorial n)

theorem expSeries_div_hasSum_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : HasSum (fun n => x ^ n / ↑(Nat.factorial n)) (exp 𝕂 x)

theorem exp_neg {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : exp 𝕂 (-x) = (exp 𝕂 x)⁻¹

theorem exp_zsmul {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (z : ℤ) (x : 𝔸) : exp 𝕂 (z • x) = exp 𝕂 x ^ z

theorem exp_conj {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (y : 𝔸) (x : 𝔸) (hy : y ≠ 0) : exp 𝕂 (y * x * y⁻¹) = y * exp 𝕂 x * y⁻¹

theorem exp_conj' {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (y : 𝔸) (x : 𝔸) (hy : y ≠ 0) : exp 𝕂 (y⁻¹ * x * y) = y⁻¹ * exp 𝕂 x * y

theorem exp_add {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {x : 𝔸} {y : 𝔸} : exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y

In a commutative Banach-algebra 𝔸 over 𝕂 = ℝ or 𝕂 = ℂ, exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y).

theorem exp_sum {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {ι : Type u_3} (s : Finset ι) (f : ι → 𝔸) : exp 𝕂 (Finset.sum s fun i => f i) = Finset.prod s fun i => exp 𝕂 (f i)

A version of exp_sum_of_commute for a commutative Banach-algebra.

theorem expSeries_eq_expSeries (𝕂 : Type u_1) (𝕂' : Type u_2) (𝔸 : Type u_3) [Field 𝕂] [Field 𝕂'] [Ring 𝔸] [Algebra 𝕂 𝔸] [Algebra 𝕂' 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (n : ℕ) (x : 𝔸) : (↑(expSeries 𝕂 𝔸 n) fun x => x) = ↑(expSeries 𝕂' 𝔸 n) fun x => x

If a normed ring 𝔸 is a normed algebra over two fields, then they define the same expSeries on 𝔸.

theorem exp_eq_exp (𝕂 : Type u_1) (𝕂' : Type u_2) (𝔸 : Type u_3) [Field 𝕂] [Field 𝕂'] [Ring 𝔸] [Algebra 𝕂 𝔸] [Algebra 𝕂' 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] : exp 𝕂 = exp 𝕂'

If a normed ring 𝔸 is a normed algebra over two fields, then they define the same exponential function on 𝔸.

theorem exp_ℝ_ℂ_eq_exp_ℂ_ℂ : exp ℝ = exp ℂ

@[simp]

theorem of_real_exp_ℝ_ℝ (r : ℝ) : ↑(exp ℝ r) = exp ℂ ↑r

A version of Complex.ofReal_exp for exp instead of Complex.exp