Commit 2022-02-15 19:34 b0fe9723
View on Github →feat (analysis/normed_space/spectrum): prove Gelfand's formula for the spectral radius (#11916)
This establishes Gelfand's formula for the spectral radius in a complex Banach algebra A, namely that the sequence of n-th roots of the norms of n-th powers of any element tends to its spectral radius. Some results which hold in more generality concerning the function z ↦ ring.inverse (1 - z • a) are also given. In particular, this function is differentiable on the disk with radius the reciprocal of the spectral radius, and it has a power series on the ball with radius equal to the reciprocal of the norm of a : A.
Currently, the version of Gelfand's formula which appears here includes an assumption that A is second countable, which won't hold in general unless A is separable. This is not a true (i.e., mathematical) limitation, but a consequence of the current implementation of Bochner integrals in mathlib (which are an essential feature in the proof of Gelfand's formula because of its use of the Cauchy integral formula). When Bochner integrals are refactored, this type class assumption can be dropped.