mathlib3

50691e59 - chore(measure_theory/function): split files strongly_measurable and simple_func_dense (#12711)

chore(measure_theory/function): split files strongly_measurable and simple_func_dense (#12711) The files `strongly_measurable` and `simple_func_dense` contain general results, and results pertaining to the `L^p` space. We move the results regarding `L^p` to new files, to make sure that the main parts of the files can be imported earlier in the hierarchy. This is needed for a forthcoming integral refactor.