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 𝕂' 𝔸

Notes

We put nearly all the statements in this file in the NormedSpace namespace, to avoid collisions with the Real or Complex namespaces.

As of 2023-11-16 due to bad instances in Mathlib

import Mathlib

open Real

#time example (x : ℝ) : 0 < exp x      := exp_pos _ -- 250ms
#time example (x : ℝ) : 0 < Real.exp x := exp_pos _ -- 2ms

This is because exp x tries the exp function defined here, and generates a slow coercion search from Real to Type, to fit the first argument here. We will resolve this slow coercion separately, but we want to move exp out of the root namespace in any case to avoid this ambiguity.

In the long term is may be possible to replace Real.exp and Complex.exp with this one.

def NormedSpace.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 𝕂 : 𝔸 → 𝔸.

Equations

• NormedSpace.expSeries 𝕂 𝔸 n = (↑(Nat.factorial n))⁻¹ • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸

noncomputable def NormedSpace.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.

Equations

• NormedSpace.exp 𝕂 x = FormalMultilinearSeries.sum (NormedSpace.expSeries 𝕂 𝔸) x

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem NormedSpace.star_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] (x : 𝔸) : star (NormedSpace.exp 𝕂 x) = NormedSpace.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 (NormedSpace.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 (NormedSpace.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 (NormedSpace.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 (NormedSpace.exp 𝕂 x) (NormedSpace.exp 𝕂 y)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem NormedSpace.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 (NormedSpace.expSeries 𝕂 𝔸))) (hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (NormedSpace.expSeries 𝕂 𝔸))) : NormedSpace.exp 𝕂 (x + y) = NormedSpace.exp 𝕂 x * NormedSpace.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 NormedSpace.invertibleExpOfMemBall {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (NormedSpace.expSeries 𝕂 𝔸))) : Invertible (NormedSpace.exp 𝕂 x)

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Any continuous ring homomorphism commutes with exp.

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

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

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

theorem NormedSpace.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 (NormedSpace.expSeries 𝕂 𝔸))) : HasSum (fun (n : ℕ) => x ^ n / ↑(Nat.factorial n)) (NormedSpace.exp 𝕂 x)

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

theorem NormedSpace.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 (NormedSpace.expSeries 𝕂 𝔸))) (hy : y ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (NormedSpace.expSeries 𝕂 𝔸))) : NormedSpace.exp 𝕂 (x + y) = NormedSpace.exp 𝕂 x * NormedSpace.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 NormedSpace.expSeries_radius_eq_top (𝕂 : Type u_1) (𝔸 : Type u_2) [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] : FormalMultilinearSeries.radius (NormedSpace.expSeries 𝕂 𝔸) = ⊤

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

• NormedSpace.invertibleExp 𝕂 x = NormedSpace.invertibleExpOfMemBall (_ : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (NormedSpace.expSeries 𝕂 𝔸)))

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

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

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

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

theorem NormedSpace.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)) : NormedSpace.exp 𝕂 (Finset.sum s fun (i : ι) => f i) = Finset.noncommProd s (fun (i : ι) => NormedSpace.exp 𝕂 (f i)) (_ : ∀ i ∈ ↑s, ∀ j ∈ ↑s, i ≠ j → Commute (NormedSpace.exp 𝕂 (f i)) (NormedSpace.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 NormedSpace.exp_nsmul {𝕂 : Type u_1} {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (n : ℕ) (x : 𝔸) : NormedSpace.exp 𝕂 (n • x) = NormedSpace.exp 𝕂 x ^ n

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

Any continuous ring homomorphism commutes with exp.

theorem NormedSpace.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 : 𝔸) : NormedSpace.exp 𝕂 (g • x) = g • NormedSpace.exp 𝕂 x

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

theorem NormedSpace.exp_units_conj' (𝕂 : Type u_1) {𝔸 : Type u_2} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (y : 𝔸ˣ) (x : 𝔸) : NormedSpace.exp 𝕂 (↑y⁻¹ * x * ↑y) = ↑y⁻¹ * NormedSpace.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 : 𝔸 × 𝔹) : (NormedSpace.exp 𝕂 x).1 = NormedSpace.exp 𝕂 x.1

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

A version of exp_sum_of_commute for a commutative Banach-algebra.

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

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

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

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

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

@[simp]

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

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