The logarithm of a product, and smoothness of the logarithm and real powers

In a Banach algebra A with an isometric continuous functional calculus, CFC.log inverts the exponential: log (exp a) = a for self-adjoint a and exp (log b) = b for strictly positive b. Since the exponential turns sums of commuting elements into products, the logarithm turns products of commuting strictly positive elements into sums, log (a * b) = log a + log b.

If the derivative TauCeti.expFDeriv 𝕂 a of the exponential is invertible at a self-adjoint a, the inverse function theorem gives an analytic local inverse of exp near exp a, and the continuity of CFC.log identifies it with CFC.log on the strictly positive elements. Hence CFC.log is C^n on the strictly positive elements for every n : ℕ∞ω, including the analytic case n = ω: near each strictly positive element it agrees on them with a function that is analytic on a whole neighbourhood in A. The real powers a ^ s = exp (s • log a) and the square root inherit this smoothness. The same identity and the continuity of CFC.log make the real powers jointly continuous in the base and the exponent.

The hypothesis on the derivative holds for matrices; see TauCeti/Analysis/Matrix/Exponential/Log.lean.

Main results

• CFC.log_mul_of_commute: log (a * b) = log a + log b for commuting strictly positive a and b.
• CFC.rpow_eq_exp_smul_log: a ^ s = exp (s • log a) for strictly positive a.
• CFC.continuousOn_rpow_prod: (a, s) ↦ a ^ s is jointly continuous on the strictly positive elements.
• CFC.contDiffWithinAt_log_exp: if expFDeriv 𝕂 a is invertible at a self-adjoint a, then CFC.log is C^n at exp a within the strictly positive elements, for every n.
• CFC.contDiffOn_log, CFC.contDiffOn_rpow, CFC.contDiffOn_sqrt: if expFDeriv 𝕂 a is invertible at every self-adjoint a, then CFC.log, every real power and the square root are C^n on the strictly positive elements.

theorem CFC.rpow_eq_exp_smul_log {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) (s : ℝ) (ha : IsStrictlyPositive a := by cfc_tac) : a ^ s = NormedSpace.exp (s • log a)

A real power of a strictly positive element is the exponential of the rescaled logarithm.

theorem CFC.log_mul_of_commute {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [CompleteSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a b : A} (hab : Commute a b) (ha : IsStrictlyPositive a := by cfc_tac) (hb : IsStrictlyPositive b := by cfc_tac) : log (a * b) = log a + log b

The logarithm of a product of commuting strictly positive elements is the sum of their logarithms.

theorem CFC.continuousOn_rpow_prod {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [CompleteSpace A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] : ContinuousOn (fun (p : A × ℝ) => p.1 ^ p.2) ({a : A | IsStrictlyPositive a} ×ˢ Set.univ)

Real powers are jointly continuous in the base and the exponent: (a, s) ↦ a ^ s is continuous on the pairs whose base is strictly positive. For a fixed exponent this is CFC.continuousOn_rpow.

theorem CFC.contDiffWithinAt_log_exp {𝕂 : Type u_1} {A : Type u_2} [RCLike 𝕂] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [NormedAlgebra 𝕂 A] [CompleteSpace A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a : A} (ha : IsSelfAdjoint a) (hda : IsUnit (TauCeti.expFDeriv 𝕂 a)) {n : WithTop ℕ∞} : ContDiffWithinAt 𝕂 n log {b : A | IsStrictlyPositive b} (NormedSpace.exp a)

If the derivative of the exponential is invertible at a self-adjoint a, then CFC.log is C^n at exp a within the strictly positive elements: near exp a it agrees on them with the analytic local inverse of exp.

theorem CFC.contDiffOn_log {𝕂 : Type u_1} {A : Type u_2} [RCLike 𝕂] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [NormedAlgebra 𝕂 A] [CompleteSpace A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (hda : ∀ (a : A), IsSelfAdjoint a → IsUnit (TauCeti.expFDeriv 𝕂 a)) {n : WithTop ℕ∞} : ContDiffOn 𝕂 n log {b : A | IsStrictlyPositive b}

If the derivative of the exponential is invertible at every self-adjoint element, then CFC.log is C^n on the strictly positive elements.

theorem CFC.contDiffOn_rpow {𝕂 : Type u_1} {A : Type u_2} [RCLike 𝕂] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [NormedAlgebra 𝕂 A] [CompleteSpace A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [SMulCommClass 𝕂 ℝ A] (hda : ∀ (a : A), IsSelfAdjoint a → IsUnit (TauCeti.expFDeriv 𝕂 a)) (s : ℝ) {n : WithTop ℕ∞} : ContDiffOn 𝕂 n (fun (a : A) => a ^ s) {b : A | IsStrictlyPositive b}

If the derivative of the exponential is invertible at every self-adjoint element, then every real power a ↦ a ^ s is C^n on the strictly positive elements.

theorem CFC.contDiffOn_sqrt {𝕂 : Type u_1} {A : Type u_2} [RCLike 𝕂] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [NormedAlgebra 𝕂 A] [CompleteSpace A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [SMulCommClass 𝕂 ℝ A] (hda : ∀ (a : A), IsSelfAdjoint a → IsUnit (TauCeti.expFDeriv 𝕂 a)) {n : WithTop ℕ∞} : ContDiffOn 𝕂 n sqrt {b : A | IsStrictlyPositive b}

If the derivative of the exponential is invertible at every self-adjoint element, then the square root is C^n on the strictly positive elements.