Documentation

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog

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 #

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 #

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 : autoParam (p a) _auto✝) :
cfc (NormedSpace.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) :
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
Instances For
    @[simp]
    @[simp]
    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₁ : autoParam (IsSelfAdjoint a) _auto✝) :
    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₁ : autoParam (IsSelfAdjoint a) _auto✝) :