I am not au courant, anybody knows something about it?
Regards,
Andrzej Trybulec
----- Przekazana wiadomość od
freek@... -----
Data: Sun, 25 Oct 2009 21:29:06 +0100
Od: freek <
freek@...>
Odpowiedz-Do:freek <
freek@...>
Temat: Re: Radon-Nikodym theorem
Do: William Faris <
faris@...>
Dear Bill Faris,
> Is there a proof in one of the current systems of the
> Radon-Nikodym theorem?
Not that I know of, but that doesn't mean _too_ much.
(I'll CC this answer to John Harrison, Andrzej Trybulec
and Bas Spitters, in case one of them _does_ know. I saw
that it's in Bas' PhD thesis, and I know Bas is working on
formalizing integration in Coq: so maybe he already has it.)
Just to satisfy my curiosity: how dificult is a textbook
proof of this theorem, on top of the basic theory about
Lebesgue integration? About one page?
Freek
----- Koniec przekazanej wiadomości -----
