Commit 2021-02-13 19:32 ac19b4a9View on Github →
refactor(measure_theory/l1_space): remove one of the two definitions of L1 space (#6058)
Currently, we have two independent versions of the
L^1 space in mathlib: one coming from the general family of
L^p spaces, the other one is an ad hoc construction based on the
integrable predicate used in the construction of the Bochner integral.
We remove the second construction, and use instead the
L^1 space coming from the family of
L^p spaces to construct the Bochner integral. Still, we keep the
integrable predicate as it is generally useful, and show that it coincides with the
mem_Lp 1 predicate.