feat(analysis/*/{exponential, spectrum}): spectrum of a selfadjoint element is real (#12417)

This provides several properties of the exponential function and uses it to prove that for `𝕜 = ℝ` or `𝕜 = ℂ`, `exp 𝕜 𝕜` maps the spectrum of `a : A` (where `A` is a `𝕜`-algebra) into the spectrum of `exp 𝕜 A a`. In addition, `exp ℂ A (I • a)` is unitary when `a` is selfadjoint. Consequently, the spectrum of a selfadjoint element is real.

Author: j-loreaux

src/analysis/normed_space/basic.lean

@@ -359,6 +359,20 @@ end
 
 variables (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜]
 
+/-- The inclusion of the base field in a normed algebra as a continuous linear map. -/
+@[simps]
+def algebra_map_clm [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] : 𝕜 →L[𝕜] 𝕜' :=
+{ to_fun := algebra_map 𝕜 𝕜',
+  map_add' := (algebra_map 𝕜 𝕜').map_add,
+  map_smul' := λ r x, by rw [algebra.id.smul_eq_mul, map_mul, ring_hom.id_apply, algebra.smul_def],
+  cont := (algebra_map_isometry 𝕜 𝕜').continuous }
+
+lemma algebra_map_clm_coe [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
+  (algebra_map_clm 𝕜 𝕜' : 𝕜 → 𝕜') = (algebra_map 𝕜 𝕜' : 𝕜 → 𝕜') := rfl
+
+lemma algebra_map_clm_to_linear_map [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
+  (algebra_map_clm 𝕜 𝕜').to_linear_map = algebra.linear_map 𝕜 𝕜' := rfl
+
 @[priority 100]
 instance normed_algebra.to_normed_space [semi_normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] :
   normed_space 𝕜 𝕜' :=

src/analysis/normed_space/exponential.lean

@@ -210,6 +210,17 @@ end
 
 end complete_algebra
 
+lemma algebra_map_exp_comm_of_mem_ball [complete_space 𝕂] (x : 𝕂)
+  (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) :
+  algebra_map 𝕂 𝔸 (exp 𝕂 𝕂 x) = exp 𝕂 𝔸 (algebra_map 𝕂 𝔸 x) :=
+begin
+  convert (algebra_map_clm 𝕂 𝔸).map_tsum (exp_series_field_summable_of_mem_ball x hx),
+  { exact congr_fun exp_eq_tsum_field x },
+  { convert congr_fun (exp_eq_tsum : exp 𝕂 𝔸 = _) (algebra_map 𝕂 𝔸 x),
+    simp_rw [←map_pow, ←algebra_map_clm_coe, ←(algebra_map_clm 𝕂 𝔸).map_smul, smul_eq_mul,
+      mul_comm, ←div_eq_mul_one_div], }
+end
+
 end any_field_any_algebra
 
 section any_field_comm_algebra
@@ -318,6 +329,10 @@ lemma exp_add_of_commute [complete_space 𝔸]
 exp_add_of_commute_of_mem_ball hxy ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
   ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
+lemma algebra_map_exp_comm (x : 𝕂) :
+  algebra_map 𝕂 𝔸 (exp 𝕂 𝕂 x) = exp 𝕂 𝔸 (algebra_map 𝕂 𝔸 x) :=
+algebra_map_exp_comm_of_mem_ball x (by simp [exp_series_radius_eq_top])
+
 end any_algebra
 
 section comm_algebra
@@ -362,3 +377,17 @@ lemma exp_ℝ_ℂ_eq_exp_ℂ_ℂ : exp ℝ ℂ = exp ℂ ℂ :=
 exp_eq_exp ℝ ℂ ℂ
 
 end scalar_tower
+
+lemma star_exp {𝕜 A : Type*} [is_R_or_C 𝕜] [normed_ring A] [normed_algebra 𝕜 A]
+  [star_ring A] [normed_star_group A] [complete_space A]
+  [star_module 𝕜 A] (a : A) : star (exp 𝕜 A a) = exp 𝕜 A (star a) :=
+begin
+  rw exp_eq_tsum,
+  have := continuous_linear_map.map_tsum
+    (starₗᵢ 𝕜 : A ≃ₗᵢ⋆[𝕜] A).to_linear_isometry.to_continuous_linear_map
+    (exp_series_summable' a),
+  dsimp at this,
+  convert this,
+  funext,
+  simp only [star_smul, star_pow, one_div, star_inv', star_nat_cast],
+end

src/analysis/normed_space/spectrum.lean

@@ -5,6 +5,7 @@ Authors: Jireh Loreaux
 -/
 import algebra.algebra.spectrum
 import analysis.special_functions.pow
+import analysis.special_functions.exponential
 import analysis.complex.liouville
 import analysis.analytic.radius_liminf
 /-!
@@ -346,6 +347,43 @@ begin
     (mem_resolvent_set_iff.mp (H₀.symm ▸ set.mem_univ 0)))),
 end
 
+section exp_mapping
+
+local notation `↑ₐ` := algebra_map 𝕜 A
+
+/-- For `𝕜 = ℝ` or `𝕜 = ℂ`, `exp 𝕜 𝕜` maps the spectrum of `a` into the spectrum of `exp 𝕜 A a`. -/
+theorem exp_mem_exp [is_R_or_C 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
+  (a : A) {z : 𝕜} (hz : z ∈ spectrum 𝕜 a) : exp 𝕜 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 A a) :=
+begin
+  have hexpmul : exp 𝕜 A a = exp 𝕜 A (a - ↑ₐ z) * ↑ₐ (exp 𝕜 𝕜 z),
+  { rw [algebra_map_exp_comm z, ←exp_add_of_commute (algebra.commutes z (a - ↑ₐz)).symm,
+      sub_add_cancel] },
+  let b := ∑' n : ℕ, ((1 / (n + 1).factorial) : 𝕜) • (a - ↑ₐz) ^ n,
+  have hb : summable (λ n : ℕ, ((1 / (n + 1).factorial) : 𝕜) • (a - ↑ₐz) ^ n),
+  { refine summable_of_norm_bounded_eventually _ (real.summable_pow_div_factorial ∥a - ↑ₐz∥) _,
+    filter_upwards [filter.eventually_cofinite_ne 0] with n hn,
+    rw [norm_smul, mul_comm, norm_div, norm_one, is_R_or_C.norm_eq_abs, is_R_or_C.abs_cast_nat,
+      ←div_eq_mul_one_div],
+    exact div_le_div (pow_nonneg (norm_nonneg _) n) (norm_pow_le' (a - ↑ₐz) (zero_lt_iff.mpr hn))
+      (by exact_mod_cast nat.factorial_pos n)
+      (by exact_mod_cast nat.factorial_le (lt_add_one n).le) },
+  have h₀ : ∑' n : ℕ, ((1 / (n + 1).factorial) : 𝕜) • (a - ↑ₐz) ^ (n + 1) = (a - ↑ₐz) * b,
+    { simpa only [mul_smul_comm, pow_succ] using hb.tsum_mul_left (a - ↑ₐz) },
+  have h₁ : ∑' n : ℕ, ((1 / (n + 1).factorial) : 𝕜) • (a - ↑ₐz) ^ (n + 1) = b * (a - ↑ₐz),
+    { simpa only [pow_succ', algebra.smul_mul_assoc] using hb.tsum_mul_right (a - ↑ₐz) },
+  have h₃ : exp 𝕜 A (a - ↑ₐz) = 1 + (a - ↑ₐz) * b,
+  { rw exp_eq_tsum,
+    convert tsum_eq_zero_add (exp_series_summable' (a - ↑ₐz)),
+    simp only [nat.factorial_zero, nat.cast_one, _root_.div_one, pow_zero, one_smul],
+    exact h₀.symm },
+  rw [spectrum.mem_iff, is_unit.sub_iff, ←one_mul (↑ₐ(exp 𝕜 𝕜 z)), hexpmul, ←_root_.sub_mul,
+    commute.is_unit_mul_iff (algebra.commutes (exp 𝕜 𝕜 z) (exp 𝕜 A (a - ↑ₐz) - 1)).symm,
+    sub_eq_iff_eq_add'.mpr h₃, commute.is_unit_mul_iff (h₀ ▸ h₁ : (a - ↑ₐz) * b = b * (a - ↑ₐz))],
+  exact not_and_of_not_left _ (not_and_of_not_left _ ((not_iff_not.mpr is_unit.sub_iff).mp hz)),
+end
+
+end exp_mapping
+
 end spectrum
 
 namespace alg_hom

src/analysis/normed_space/star/exponential.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2022 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+import analysis.normed_space.star.basic
+import algebra.star.module
+import analysis.special_functions.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.
+-/
+
+section star
+
+variables {A : Type*}
+[normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [complete_space A]
+[star_module ℂ A]
+
+open complex
+
+lemma self_adjoint.exp_i_smul_unitary {a : A} (ha : a ∈ self_adjoint A) :
+  exp ℂ A (I • a) ∈ unitary A :=
+begin
+  rw [unitary.mem_iff, star_exp],
+  simp only [star_smul, is_R_or_C.star_def, self_adjoint.mem_iff.mp ha, conj_I, neg_smul],
+  rw ←@exp_add_of_commute ℂ A _ _ _ _ _ _ ((commute.refl (I • a)).neg_left),
+  rw ←@exp_add_of_commute ℂ A _ _ _ _ _ _ ((commute.refl (I • a)).neg_right),
+  simpa only [add_right_neg, add_left_neg, and_self] using (exp_zero : exp ℂ A 0 = 1),
+end
+
+/-- The map from the selfadjoint real subspace to the unitary group. This map only makes sense
+over ℂ. -/
+@[simps]
+noncomputable def self_adjoint.exp_unitary (a : self_adjoint A) : unitary A :=
+⟨exp ℂ A (I • a), self_adjoint.exp_i_smul_unitary (a.property)⟩
+
+open self_adjoint
+
+lemma commute.exp_unitary_add {a b : self_adjoint A} (h : commute (a : A) (b : A)) :
+  exp_unitary (a + b) = exp_unitary a * exp_unitary b :=
+begin
+  ext,
+  have hcomm : commute (I • (a : A)) (I • (b : A)),
+  calc _ = _ : by simp only [h.eq, algebra.smul_mul_assoc, algebra.mul_smul_comm],
+  simpa only [exp_unitary_coe, add_subgroup.coe_add, smul_add] using exp_add_of_commute hcomm,
+end
+
+lemma commute.exp_unitary {a b : self_adjoint A} (h : commute (a : A) (b : A)) :
+  commute (exp_unitary a) (exp_unitary b) :=
+calc (exp_unitary a) * (exp_unitary b) = (exp_unitary b) * (exp_unitary a)
+  : by rw [←h.exp_unitary_add, ←h.symm.exp_unitary_add, add_comm]
+
+end star

src/analysis/normed_space/star/spectrum.lean

@@ -5,6 +5,8 @@ Authors: Jireh Loreaux
 -/
 import analysis.normed_space.star.basic
 import analysis.normed_space.spectrum
+import algebra.star.module
+import analysis.normed_space.star.exponential
 
 /-! # Spectral properties in C⋆-algebras
 In this file, we establish various propreties related to the spectrum of elements in C⋆-algebras.
@@ -42,11 +44,15 @@ end unitary_spectrum
 
 section complex_scalars
 
+open complex
+
 variables {A : Type*}
-[normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [complete_space A]
-[measurable_space A] [borel_space A] [topological_space.second_countable_topology A]
+[normed_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] [cstar_ring A]
+
+local notation `↑ₐ` := algebra_map ℂ A
 
-lemma spectral_radius_eq_nnnorm_of_self_adjoint {a : A} (ha : a ∈ self_adjoint A) :
+lemma spectral_radius_eq_nnnorm_of_self_adjoint [measurable_space A] [borel_space A]
+  [topological_space.second_countable_topology A] {a : A} (ha : a ∈ self_adjoint A) :
   spectral_radius ℂ a = ∥a∥₊ :=
 begin
   have hconst : tendsto (λ n : ℕ, (∥a∥₊ : ℝ≥0∞)) at_top _ := tendsto_const_nhds,
@@ -59,7 +65,8 @@ begin
   simp,
 end
 
-lemma spectral_radius_eq_nnnorm_of_star_normal (a : A) [is_star_normal a] :
+lemma spectral_radius_eq_nnnorm_of_star_normal [topological_space.second_countable_topology A]
+  [measurable_space A] [borel_space A] (a : A) [is_star_normal a] :
   spectral_radius ℂ a = ∥a∥₊ :=
 begin
   refine (ennreal.pow_strict_mono (by linarith : 2 ≠ 0)).injective _,
@@ -77,4 +84,35 @@ begin
   rw [spectral_radius_eq_nnnorm_of_self_adjoint ha, sq, nnnorm_star_mul_self, coe_mul],
 end
 
+/-- Any element of the spectrum of a selfadjoint is real. -/
+theorem self_adjoint.mem_spectrum_eq_re [star_module ℂ A] [nontrivial A] {a : A}
+  (ha : a ∈ self_adjoint A) {z : ℂ} (hz : z ∈ spectrum ℂ a) : z = z.re :=
+begin
+  let Iu := units.mk0 I I_ne_zero,
+  have : exp ℂ ℂ (I • z) ∈ spectrum ℂ (exp ℂ A (I • a)),
+    by simpa only [units.smul_def, units.coe_mk0]
+      using spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz),
+  exact complex.ext (of_real_re _)
+    (by simpa only [←complex.exp_eq_exp_ℂ_ℂ, mem_sphere_zero_iff_norm, norm_eq_abs, abs_exp,
+      real.exp_eq_one_iff, smul_eq_mul, I_mul, neg_eq_zero]
+      using spectrum.subset_circle_of_unitary (self_adjoint.exp_i_smul_unitary ha) this),
+end
+
+/-- Any element of the spectrum of a selfadjoint is real. -/
+theorem self_adjoint.mem_spectrum_eq_re' [star_module ℂ A] [nontrivial A]
+  (a : self_adjoint A) {z : ℂ} (hz : z ∈ spectrum ℂ (a : A)) : z = z.re :=
+self_adjoint.mem_spectrum_eq_re a.property hz
+
+/-- The spectrum of a selfadjoint is real -/
+theorem self_adjoint.coe_re_map_spectrum [star_module ℂ A] [nontrivial A] {a : A}
+  (ha : a ∈ self_adjoint A) : spectrum ℂ a = (coe ∘ re '' (spectrum ℂ a) : set ℂ) :=
+le_antisymm (λ z hz, ⟨z, hz, (self_adjoint.mem_spectrum_eq_re ha hz).symm⟩) (λ z, by
+  { rintros ⟨z, hz, rfl⟩,
+    simpa only [(self_adjoint.mem_spectrum_eq_re ha hz).symm, function.comp_app] using hz })
+
+/-- The spectrum of a selfadjoint is real -/
+theorem self_adjoint.coe_re_map_spectrum' [star_module ℂ A] [nontrivial A] (a : self_adjoint A) :
+  spectrum ℂ (a : A) = (coe ∘ re '' (spectrum ℂ (a : A)) : set ℂ) :=
+self_adjoint.coe_re_map_spectrum a.property
+
 end complex_scalars