README.md

Measure Integration

This formalization includes properties about Sigma algebras, measures, the Fubini-Tonelli Lemmas, etc. It is mainly based on "Fundamentals of Real Analysis" by Sterling K. Berberian (Springer, 1991).

Highlights

Major theorems

Theorem	Location	PVS Name	Contributors
Fubini-Tonelli Lemmas	measure_integration@fubini_tonelli	fubini_tonelli_*	David Lester

Contributors

• David Lester, Manchester University, UK
• César Muñoz, NASA, USA
• Mariano Moscato, NIA & NASA, USA
• Sam Owre, SRI, USA

Maintainer

• César Muñoz, NASA, USA

Dependencies