[mizar] Fwd: Re: Radon-Nikodym theorem

[trybulec@math.uwb.edu.pl]

I am not au courant, anybody knows something about it?

Regards,
Andrzej Trybulec

----- Przekazana wiadomość od freek@cs.ru.nl -----
   Data: Sun, 25 Oct 2009 21:29:06 +0100
   Od: freek <freek@cs.ru.nl>
Odpowiedz-Do:freek <freek@cs.ru.nl>
Temat: Re: Radon-Nikodym theorem
     Do: William Faris <faris@math.arizona.edu>

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 -----