Commit 2021-02-13 19:32 ac19b4a9

View 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.

Estimated changes

deleted theorem measure_theory.l1.coe_add
deleted theorem measure_theory.l1.coe_coe
deleted theorem measure_theory.l1.coe_neg
deleted theorem measure_theory.l1.coe_sub
deleted theorem measure_theory.l1.dist_eq
deleted theorem measure_theory.l1.norm_eq
deleted def measure_theory.l1