Commit 2024-07-17 03:09 f27bf519

View on Github →

feat(ContinuousFunctionalCalculus): Define the real log based on the CFC (#14448) This PR defines CFC.log as cfc Real.log, and shows its basic properties, such as the fact that it's the inverse of NormedSpace.exp ℝ. Along the way, we also show that the exponential defined via the CFC is equal to NormedSpace.exp, which is defined via power series.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean

added theorem CFC.complex_exp_eq_normedSpace_exp

added theorem CFC.exp_eq_normedSpace_exp

added theorem CFC.exp_log

added theorem CFC.log_algebraMap

added theorem CFC.log_exp

added theorem CFC.log_one

added theorem CFC.log_pow

added theorem CFC.log_smul

added theorem CFC.log_zero

added theorem CFC.real_exp_eq_normedSpace_exp

added theorem NormedSpace.exp_continuousMap_eq

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean

added theorem cfc_add_const

added theorem cfc_const_add