Commit 2021-03-28 19:54 a17f38f2

View on Github →

feat(measure_theory/lp_space): bounded continuous functions are in Lp (#6878) Under appropriate conditions (finite Borel measure, second-countable), a bounded continuous function is in L^p. The main result of this PR is bounded_continuous_function.to_Lp, which provides this operation as a bounded linear map. There are also several variations.

Estimated changes