@MISC{MESFUN12.MIZ,
  AUTHOR = {Endou, Noboru},
  TITLE = {Fubini's Theorem for Nonnegative or Nonpositive Functions},
  DAY = {27},
  MONTH = {March},
  YEAR = {2018},
  ADDRESS1 = {National Institute of Technology, Gifu College\\2236-2 Kamimakuwa, Motosu, Gifu, Japan},
  SECTION1 = {Extended real valued characteristic function},
  SECTION2 = {Some properties of integration},
  SECTION3 = {Sections of partial function},
  SECTION4 = {Fubini's theorem for nonnegative or nonpositive functions},
  SUMMARY = {The goal of this article is to show Fubini's
  theorem for nonnegative or nonpositive measurable functions
  \cite{Halmos74}, \cite{Bauer:2002}, \cite{Bogachev2007measure}.
  We formalized Fubini's theorem in our previous article \cite{MEASUR11.ABS},
  but in that case we showed the Fubini's theorem for measurable sets
  and it was not enough as the integral does not appear explicitly.
  On the other hand, the theorems obtained in this paper are more general
  and it can be easily extended to a general integrable function.
  Furthermore, it also can be easy to extend to functional space $L^p$
  \cite{LPSPACE1.ABS}. It should be mentioned also that H{\"o}lzl and Heller
  \cite{hoelzl2011measuretheory} have introduced the Lebesgue integration
  theory in Isabelle/HOL and have proved Fubini's theorem there.}}

@inproceedings{hoelzl2011measuretheory,
  author       = {Johannes H{\"o}lzl and Armin Heller},
  title        = {Three Chapters of Measure Theory in {Isabelle/HOL}},
  year         = {2011},
  pages        = {135-151},
  editor       = {Marko C. J. D. van Eekelen and Herman Geuvers and Julien Schmaltz and Freek Wiedijk},
  booktitle    = {Interactive Theorem Proving (ITP 2011)},
  series       = {LNCS},
  volume       = {6898}}

