Lp spaces

Title:	Lp spaces
Author:	Sebastien Gouezel
Submission date:	2016-10-05
Abstract:	Lp is the space of functions whose p-th power is integrable. It is one of the most fundamental Banach spaces that is used in analysis and probability. We develop a framework for function spaces, and then implement the Lp spaces in this framework using the existing integration theory in Isabelle/HOL. Our development contains most fundamental properties of Lp spaces, notably the Hölder and Minkowski inequalities, completeness of Lp, duality, stability under almost sure convergence, multiplication of functions in Lp and Lq, stability under conditional expectation.
BibTeX:	@article{Lp-AFP, author = {Sebastien Gouezel}, title = {Lp spaces}, journal = {Archive of Formal Proofs}, month = oct, year = 2016, note = {\url{http://isa-afp.org/entries/Lp.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Ergodic_Theory
Used by:	Fourier
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.