Documentation

Mathlib.Analysis.Normed.Algebra.Exponential

Exponential in a Banach algebra #

In this file, we define NormedSpace.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 NormedSpace.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 #

𝕂 = ℝ or 𝕂 = ℂ #

Other useful compatibility results #

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 NormedSpace.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 𝔸] :

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

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

    NormedSpace.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.Normed.Algebra.MatrixExponential for lemmas specific to that case.

    Equations
    Instances For
      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) = (↑n.factorial)⁻¹ 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 : ) => (↑n.factorial)⁻¹ x ^ n
      theorem NormedSpace.expSeries_sum_eq {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (x : 𝔸) :
      (NormedSpace.expSeries 𝕂 𝔸).sum x = ∑' (n : ), (↑n.factorial)⁻¹ x ^ n
      theorem NormedSpace.exp_eq_tsum {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] :
      NormedSpace.exp 𝕂 = fun (x : 𝔸) => ∑' (n : ), (↑n.factorial)⁻¹ 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 𝔸] :
      @[simp]
      theorem NormedSpace.exp_op {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] (x : 𝔸) :
      @[simp]
      theorem NormedSpace.exp_unop {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] (x : 𝔸ᵐᵒᵖ) :
      theorem NormedSpace.star_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] (x : 𝔸) :
      theorem IsSelfAdjoint.exp (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] {x : 𝔸} (h : IsSelfAdjoint x) :
      theorem Commute.exp_right (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] {x : 𝔸} {y : 𝔸} (h : Commute x y) :
      theorem Commute.exp_left (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] {x : 𝔸} {y : 𝔸} (h : Commute x y) :
      theorem Commute.exp (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [T2Space 𝔸] {x : 𝔸} {y : 𝔸} (h : Commute x 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 / n.factorial
      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 / n.factorial
      theorem NormedSpace.expSeries_sum_eq_div {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [DivisionRing 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] (x : 𝔸) :
      (NormedSpace.expSeries 𝕂 𝔸).sum x = ∑' (n : ), x ^ n / n.factorial
      theorem NormedSpace.exp_eq_tsum_div {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [DivisionRing 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] :
      NormedSpace.exp 𝕂 = fun (x : 𝔸) => ∑' (n : ), x ^ n / n.factorial
      theorem NormedSpace.norm_expSeries_summable_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) (hx : x EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) :
      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 (NormedSpace.expSeries 𝕂 𝔸).radius) :
      Summable fun (n : ) => (↑n.factorial)⁻¹ 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 (NormedSpace.expSeries 𝕂 𝔸).radius) :
      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 (NormedSpace.expSeries 𝕂 𝔸).radius) :
      Summable fun (n : ) => (↑n.factorial)⁻¹ 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 (NormedSpace.expSeries 𝕂 𝔸).radius) :
      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 (NormedSpace.expSeries 𝕂 𝔸).radius) :
      HasSum (fun (n : ) => (↑n.factorial)⁻¹ x ^ n) (NormedSpace.exp 𝕂 x)
      theorem NormedSpace.continuousOn_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] :
      theorem NormedSpace.analyticAt_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) :
      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 (NormedSpace.expSeries 𝕂 𝔸).radius) (hy : y EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) :

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

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

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

      Equations
      Instances For
        theorem NormedSpace.isUnit_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) :
        theorem NormedSpace.invOf_exp_of_mem_ball {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) [Invertible (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 (NormedSpace.expSeries 𝕂 𝔸).radius) :
        f (NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 (f x)

        Any continuous ring homomorphism commutes with NormedSpace.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 (NormedSpace.expSeries 𝕂 𝕂).radius) :
        (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 (NormedSpace.expSeries 𝕂 𝔸).radius) :
        Summable fun (n : ) => x ^ n / n.factorial
        theorem NormedSpace.expSeries_div_summable_of_mem_ball (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) :
        Summable fun (n : ) => x ^ n / n.factorial
        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 (NormedSpace.expSeries 𝕂 𝔸).radius) :
        HasSum (fun (n : ) => x ^ n / n.factorial) (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 (NormedSpace.expSeries 𝕂 𝔸).radius) :
        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 (NormedSpace.expSeries 𝕂 𝔸).radius) (hy : y EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) :

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

        theorem NormedSpace.expSeries_radius_eq_top (𝕂 : Type u_1) (𝔸 : Type u_2) [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] :
        (NormedSpace.expSeries 𝕂 𝔸).radius =

        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) [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] :
        0 < (NormedSpace.expSeries 𝕂 𝔸).radius
        theorem NormedSpace.norm_expSeries_summable {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [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} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) :
        Summable fun (n : ) => (↑n.factorial)⁻¹ x ^ n
        theorem NormedSpace.expSeries_summable {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [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} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) :
        Summable fun (n : ) => (↑n.factorial)⁻¹ x ^ n
        theorem NormedSpace.expSeries_hasSum_exp {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [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} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) :
        HasSum (fun (n : ) => (↑n.factorial)⁻¹ x ^ n) (NormedSpace.exp 𝕂 x)
        theorem NormedSpace.exp_hasFPowerSeriesAt_zero {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] :
        theorem NormedSpace.exp_continuous {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] :
        theorem Filter.Tendsto.exp {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {α : Type u_4} {l : Filter α} {f : α𝔸} {a : 𝔸} (hf : Filter.Tendsto f l (nhds a)) :
        Filter.Tendsto (fun (x : α) => NormedSpace.exp 𝕂 (f x)) l (nhds (NormedSpace.exp 𝕂 a))
        theorem NormedSpace.exp_analytic {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) :
        theorem NormedSpace.exp_add_of_commute {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {x : 𝔸} {y : 𝔸} (hxy : Commute x y) :

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

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

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

        Equations
        Instances For
          theorem NormedSpace.isUnit_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) :
          theorem NormedSpace.invOf_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) [Invertible (NormedSpace.exp 𝕂 x)] :
          theorem Ring.inverse_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) :
          theorem NormedSpace.exp_mem_unitary_of_mem_skewAdjoint (𝕂 : Type u_1) {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] {x : 𝔸} (h : x skewAdjoint 𝔸) :
          theorem NormedSpace.exp_sum_of_commute {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {ι : Type u_4} (s : Finset ι) (f : ι𝔸) (h : (↑s).Pairwise fun (i j : ι) => Commute (f i) (f j)) :
          NormedSpace.exp 𝕂 (∑ is, f i) = s.noncommProd (fun (i : ι) => NormedSpace.exp 𝕂 (f i))

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

          theorem NormedSpace.exp_nsmul {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [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} [RCLike 𝕂] [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 NormedSpace.exp.

          theorem NormedSpace.exp_smul (𝕂 : Type u_1) {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {G : Type u_4} [Monoid G] [MulSemiringAction G 𝔸] [ContinuousConstSMul G 𝔸] (g : G) (x : 𝔸) :
          theorem NormedSpace.exp_units_conj (𝕂 : Type u_1) {𝔸 : Type u_2} [RCLike 𝕂] [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} [RCLike 𝕂] [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} [RCLike 𝕂] [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} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [NormedRing 𝔹] [NormedAlgebra 𝕂 𝔹] [CompleteSpace 𝔸] [CompleteSpace 𝔹] (x : 𝔸 × 𝔹) :
          (NormedSpace.exp 𝕂 x).2 = NormedSpace.exp 𝕂 x.2
          @[simp]
          theorem Pi.coe_exp (𝕂 : Type u_1) [RCLike 𝕂] {ι : 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) [RCLike 𝕂] {ι : 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) [RCLike 𝕂] {ι : Type u_4} {𝔸 : ιType u_5} [Finite ι] [DecidableEq ι] [(i : ι) → NormedRing (𝔸 i)] [(i : ι) → NormedAlgebra 𝕂 (𝔸 i)] [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i) (j : ι) (xj : 𝔸 j) :
          theorem NormedSpace.algebraMap_exp_comm {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝕂) :
          (algebraMap 𝕂 𝔸) (NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 ((algebraMap 𝕂 𝔸) x)
          theorem NormedSpace.norm_expSeries_div_summable (𝕂 : Type u_1) {𝔸 : Type u_2} [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) :
          Summable fun (n : ) => x ^ n / n.factorial
          theorem NormedSpace.expSeries_div_summable (𝕂 : Type u_1) {𝔸 : Type u_2} [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) :
          Summable fun (n : ) => x ^ n / n.factorial
          theorem NormedSpace.expSeries_div_hasSum_exp (𝕂 : Type u_1) {𝔸 : Type u_2} [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) :
          HasSum (fun (n : ) => x ^ n / n.factorial) (NormedSpace.exp 𝕂 x)
          theorem NormedSpace.exp_neg {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) :
          theorem NormedSpace.exp_zsmul {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (z : ) (x : 𝔸) :
          NormedSpace.exp 𝕂 (z x) = NormedSpace.exp 𝕂 x ^ z
          theorem NormedSpace.exp_conj {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [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} [RCLike 𝕂] [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} [RCLike 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {x : 𝔸} {y : 𝔸} :

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

          theorem NormedSpace.exp_sum {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {ι : Type u_3} (s : Finset ι) (f : ι𝔸) :
          NormedSpace.exp 𝕂 (∑ is, f i) = is, NormedSpace.exp 𝕂 (f i)

          A version of NormedSpace.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 𝔸] :

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