gelfand formula

Stream: maths

[Jireh Loreaux]

After a month hiatus to get the semester started, I finally have a proof of the Gelfand formula for the spectral radius (woot!). However, because I needed the Cauchy integral formula (more specifically docs#differentiable_on.has_fpower_series_on_ball), I had to assume the algebra had a second countable topology. Of course, in general this won't be true unless the algebra is separable. For instance, the algebra of bounded operators on a Hilbert space isn't second countable. @Yury G. Kudryashov, any hope of removing that assumption without too much pain?

[Yury G. Kudryashov]

We only define the Bochner integral if the codomain has second countable topology. @Sebastien Gouezel was going to redefine it using strong measurability instead.

[Kevin Buzzard]

Oof. Is this going to be an issue?

[Sebastien Gouezel]

Yes, that's the next important thing on my Lean todo list, once I am done with the change of variables formula. Except that the change of variable formula is taking me into unexpected directions -- to get a completely satisfactory formulation, I need to know that a continuous injective map sends Borel sets to Borel sets, which is a nontrivial theorem in descriptive set theory and requires a good deal of prerequisites on Polish spaces and analytic sets...

[Patrick Massot]

To you really intend to prove that Borel set stuff?

[Patrick Massot]

That would probably crush our current record of overpowered proofs when specializing to integration of smooth functions on a square in $\mathbb{R}^2$.

[Jireh Loreaux]

This shouldn't be a problem for me anytime soon. It just means that certain explicit algebras can't yet be shown to satisfy the Gelfand formula, but that shouldn't prevent developing the theory anyway. Thanks!

[Sebastien Gouezel]

Yes, I'm on it. It's probably the first time I'm learning new math to formalize it in Lean!

[Yury G. Kudryashov]

What statement do you want to get?

[Sebastien Gouezel]

For the change of variables? If s is a measurable set in a finite-dimensional real vector space E, and f : E -> E has a differential f' within a set s and is injective on s, then f '' s is measurable, and its measure is given by the integral of abs (det f' x) on s. And then you deduce that the integral of any function g on f '' s is the same as the integral of g o f * abs (det f' x) on s

[Sebastien Gouezel]

Warning: under these assumptions, det f' x is not guaranteed to be measurable, even on s, but it is almost everywhere measurable there thanks to a Lebesgue density point argument, which is enough for everything. And the final formula holds without measurability or integrability assumptions on g...

[Sebastien Gouezel]

Did you know that if you consider a Borel measurable set s in a Polish space, then there exists a finer topology for which the space is still Polish, with the same Borel sets as the original topology, and for which s becomes clopen? I didn't know that until a few weeks ago, and this fact turns out to be very useful for many things, including the change of variables formula :-)

[Reid Barton]

Sebastien I have been learning a bit about this subject over the past few days for completely different reasons, so I will be rooting you on at least :halo: