Fwd: Re: Radon-Nikodym theorem
| Newsgroups | gmane.comp.mathematics.mizar,gmane.spam.detected |
|---|---|
| Message-ID | <[email protected]> |
I am not au courant, anybody knows something about it? Regards, Andrzej Trybulec ----- Przekazana wiadomość od [email protected] ----- Data: Sun, 25 Oct 2009 21:29:06 +0100 Od: freek <[email protected]> Odpowiedz-Do:freek <[email protected]> Temat: Re: Radon-Nikodym theorem Do: William Faris <[email protected]> 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 -----