The logarithm in a topological algebra #
In this file we define NormedSpace.log : πΈ β πΈ, the logarithm
log x = ββ ((-1) ^ (n + 1) / n) β’ (x - 1) ^ n in a topological ring πΈ, following the
development style of NormedSpace.exp (see Mathlib/Analysis/Normed/Algebra/Exponential.lean).
It is the value at x - 1 of the FormalMultilinearSeries NormedSpace.logSeries β πΈ, where the
β-algebra structure on πΈ is chosen using Classical.choice. It takes the junk value 0
if the series does not converge or if πΈ has no β-algebra structure (equivalently,
if 1 / n doesn't correspond to what a mathematician thinks).
This file only contains the definition and its immediate algebraic properties; convergence of
the series and the relation to NormedSpace.exp are left to later files.
Main definitions #
NormedSpace.logSeries π πΈ: the formal multilinear series whosen-th term is(xα΅’) β¦ ((-1) ^ (n + 1) / n : π) β’ β xα΅’; its sum atx - 1islog x.NormedSpace.log: the logarithmπΈ β πΈ.
Main results #
NormedSpace.log_eq_tsum:logas atsum.NormedSpace.log_one,NormedSpace.log_op,NormedSpace.star_log,NormedSpace.log_mem,Commute.log: immediate properties.
TODO #
- Ultrametric convergence: if
Kis a complete ultrametric normed field of characteristic zero then the series converges on the whole discβx - 1β < 1(no choice of prime is needed: the natural numbers of norm< 1form a prime ideal ofβ, and if it ispβthenβnβ = βpβ ^ padicValNat p n). - If moreover
β(p : K)β < 1for a primep, Iwasawa's formulalog x = lim (x ^ p ^ k - 1) / p ^ kgiveslog (x * y) = log x + log yon that disc, hencelog_inv,log_pow,log_zpowetc. - The formal identity
log ((1 + X) * (1 + Y)) = log (1 + X) + log (1 + Y)inββ¦X, Yβ§. - Relation with
NormedSpace.exp:exp (log x) = xandlog (exp x) = xwhenever both series converge. - In the ultrametric case, the computation of where the series for exp and log converge
(
βx - 1β ^ (p - 1) < β(p : K)βfor log). βlog xβ = βx - 1βwhen the series converges- Analyticity:
HasFPowerSeriesOnBall log (logSeries π πΈ) 1 (logSeries π πΈ).radiusand its consequences, mirroringNormedSpace.analyticAt_exp_of_mem_ball. - Over
βandβ,NormedSpace.logagrees withReal.logandComplex.logonβx - 1β < 1. - Analytic continuation of
login the ultrametric case (probably best to be opinionated and definelog p = 0so we get a "canonical branch" analogous to how mathlib has chosen a branch ofComplex.log).
logSeries π πΈ is the FormalMultilinearSeries whose n-th term is the map
(xα΅’) : πΈβΏ β¦ ((-1) ^ (n + 1) / n : π) β’ β xα΅’; its 0-th term is 0 since 1 / 0 = 0.
The corresponding sum evaluated at x - 1 is the logarithm NormedSpace.log x.
Equations
- NormedSpace.logSeries π πΈ n = ((-1) ^ (n + 1) / βn) β’ ContinuousMultilinearMap.mkPiAlgebraFin π n πΈ
Instances For
NormedSpace.log : πΈ β πΈ is the logarithm log x = ββ ((-1) ^ (n + 1) / n) β’ (x - 1) ^ n.
It is defined as the sum of the FormalMultilinearSeries logSeries β πΈ at x - 1, in the same
way as NormedSpace.exp, and takes the junk value 0 where the series does not converge.
If πΈ can't be equipped with a β-algebra structure, we use the junk value 0.
Equations
- NormedSpace.log x = if h : Nonempty (Algebra β πΈ) then (NormedSpace.logSeries β πΈ).sum (x - 1) else 0
Instances For
The junk value when πΈ can't be equipped with a β-algebra structure.
A subring of πΈ that is closed topologically and under β-scaling is closed under log.