# mathlibdocumentation

analysis.normed_space.star.exponential

# The exponential map from selfadjoint to unitary #

In this file, we establish various propreties related to the map λ a, exp ℂ A (I • a) between the subtypes self_adjoint A and unitary A.

## TODO #

• Show that any exponential unitary is path-connected in unitary A to 1 : unitary A.
• Prove any unitary whose distance to 1 : unitary A is less than 1 can be expressed as an exponential unitary.
• A unitary is in the path component of 1 if and only if it is a finite product of exponential unitaries.
theorem self_adjoint.exp_i_smul_unitary {A : Type u_1} [normed_ring A] [ A] [star_ring A] [ A] {a : A} (ha : a ) :
@[simp]
theorem self_adjoint.exp_unitary_coe {A : Type u_1} [normed_ring A] [ A] [star_ring A] [ A] (a : (self_adjoint A)) :
noncomputable def self_adjoint.exp_unitary {A : Type u_1} [normed_ring A] [ A] [star_ring A] [ A] (a : (self_adjoint A)) :

The map from the selfadjoint real subspace to the unitary group. This map only makes sense over ℂ.

Equations
theorem commute.exp_unitary_add {A : Type u_1} [normed_ring A] [ A] [star_ring A] [ A] {a b : (self_adjoint A)} (h : b) :
theorem commute.exp_unitary {A : Type u_1} [normed_ring A] [ A] [star_ring A] [ A] {a b : (self_adjoint A)} (h : b) :