The exponential and logarithm based on the continuous functional calculus

This file defines the logarithm via the continuous functional calculus (CFC) and builds its API. This allows one to take logs of matrices, operators, elements of a C⋆-algebra, etc.

It also shows that exponentials defined via the continuous functional calculus are equal to NormedSpace.exp (defined via power series) whenever the former are not junk values.

Main declarations

• CFC.log: the real log function based on the CFC, i.e. cfc Real.log
• CFC.exp_eq_normedSpace_exp: exponentials based on the CFC are equal to exponentials based on power series.
• CFC.log_exp and CFC.exp_log: CFC.log and NormedSpace.exp ℝ are inverses of each other.

Implementation notes

Since cfc Real.exp and cfc Complex.exp are strictly less general than NormedSpace.exp (defined via power series), we only give minimal API for these here in order to relate NormedSpace.exp to functions defined via the CFC. In particular, we don't give separate definitions for them.

TODO

• Show that log (a * b) = log a + log b whenever a and b commute (and the same for indexed products).
• Relate CFC.log to rpow, zpow, sqrt, inv.

theorem NormedSpace.exp_continuousMap_eq {𝕜 : Type u_1} {α : Type u_2} [RCLike 𝕜] [TopologicalSpace α] [CompactSpace α] (f : C(α, 𝕜)) : NormedSpace.exp 𝕜 f = { toFun := NormedSpace.exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ }

theorem CFC.exp_eq_normedSpace_exp {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] {p : A → Prop} [NormedRing A] [StarRing A] [TopologicalRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [ContinuousFunctionalCalculus 𝕜 p] {a : A} (ha : p a := by cfc_tac) : cfc (NormedSpace.exp 𝕜) a = NormedSpace.exp 𝕜 a

theorem CFC.real_exp_eq_normedSpace_exp {A : Type u_1} [NormedRing A] [StarRing A] [TopologicalRing A] [NormedAlgebra ℝ A] [CompleteSpace A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] {a : A} (ha : IsSelfAdjoint a := by cfc_tac) : cfc Real.exp a = NormedSpace.exp ℝ a

theorem IsSelfAdjoint.exp_nonneg {A : Type u_1} [NormedRing A] [StarRing A] [TopologicalRing A] [NormedAlgebra ℝ A] [CompleteSpace A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] {𝕜 : Type u_2} [Field 𝕜] [Algebra 𝕜 A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : IsSelfAdjoint a) : 0 ≤ NormedSpace.exp 𝕜 a

theorem CFC.complex_exp_eq_normedSpace_exp {A : Type u_1} {p : A → Prop} [NormedRing A] [StarRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [ContinuousFunctionalCalculus ℂ p] {a : A} (ha : p a := by cfc_tac) : cfc Complex.exp a = NormedSpace.exp ℂ a

noncomputable def CFC.log {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] (a : A) : A

The real logarithm, defined via the continuous functional calculus. This can be used on matrices, operators on a Hilbert space, elements of a C⋆-algebra, etc.

Equations

• CFC.log a = cfc Real.log a

@[simp]

theorem IsSelfAdjoint.log {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] {a : A} : IsSelfAdjoint (CFC.log a)

@[simp]

theorem CFC.log_zero {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] : CFC.log 0 = 0

@[simp]

theorem CFC.log_one {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] : CFC.log 1 = 0

@[simp]

theorem CFC.log_algebraMap {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] {r : ℝ} : CFC.log ((algebraMap ℝ A) r) = (algebraMap ℝ A) (Real.log r)

theorem CFC.log_smul {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueContinuousFunctionalCalculus ℝ A] {r : ℝ} (a : A) (ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x) (hr : 0 < r) (ha₁ : IsSelfAdjoint a := by cfc_tac) : CFC.log (r • a) = (algebraMap ℝ A) (Real.log r) + CFC.log a

theorem CFC.log_pow {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueContinuousFunctionalCalculus ℝ A] (n : ℕ) (a : A) (ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x) (ha₁ : IsSelfAdjoint a := by cfc_tac) : CFC.log (a ^ n) = n • CFC.log a

theorem CFC.log_exp {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueContinuousFunctionalCalculus ℝ A] [CompleteSpace A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) : CFC.log (NormedSpace.exp ℝ a) = a

theorem CFC.exp_log {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueContinuousFunctionalCalculus ℝ A] [CompleteSpace A] (a : A) (ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x) (ha₁ : IsSelfAdjoint a := by cfc_tac) : NormedSpace.exp ℝ (CFC.log a) = a