mathlib3

287a69a0 - refactor(measure_theory/function/uniform_integrable): change `uniform_integrable` to only require `ae_strongly_measurable` (#15623)

refactor(measure_theory/function/uniform_integrable): change `uniform_integrable` to only require `ae_strongly_measurable` (#15623) The L¹ version of the strong LLN does not require `strongly_measurable` but the assumption in `uniform_integrable` forces it to have this condition if not requiring an extra step to relax the condition (see #15392). This PR relaxes the definition of `uniform_integrable` so it only requires `ae_strongly_measurable`.