mathlib3

a17f38f2 - feat(measure_theory/lp_space): bounded continuous functions are in Lp (#6878)

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.