mathlib

24e0c854 - chore(measure_theory/{integral/set_integral,function/*}): split out inner product space material (#19019)

chore(measure_theory/{integral/set_integral,function/*}): split out inner product space material (#19019) Split out inner product space material from ```text measure_theory/function/lp_space measure_theory/function/l1_space measure_theory/integral/set_integral ``` into `measure_theory/integral/l2_space`, the only place it's used. This removes the dependence of the Bochner integral file on `inner_product_space`.