Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/6833
Tytuł: | Fubini’s Theorem for Non-Negative or Non-Positive Functions |
Autorzy: | Endou, Noboru |
Słowa kluczowe: | Fubini’ s theorem extended real-valued non-negative (or non-positive) measurable function |
Data wydania: | 2018 |
Data dodania: | 20-sie-2018 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 26, Issue 1, Pages 49–67 |
Abstrakt: | The goal of this article is to show Fubini’s theorem for non-negative or non-positive measurable functions [10], [2], [3], using the Mizar system [1], [9]. We formalized Fubini’s theorem in our previous article [5], 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 Lp [12]. It should be mentioned also that Hölzl and Heller [11] have introduced the Lebesgue integration theory in Isabelle/HOL and have proved Fubini’s theorem there. |
Afiliacja: | National Institute of Technology, Gifu College, 2236-2 Kamimakuwa, Motosu, Gifu, Japan |
URI: | http://hdl.handle.net/11320/6833 |
DOI: | 10.2478/forma-2018-0005 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Formalized Mathematics, 2018, Volume 26, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2018-0005.pdf | 313,49 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL