Commit 2022-11-13 16:06 d3b69f63

View on Github →

refactor(measure_theory/function/special_functions): split to reduce imports (#17512) This will move a few files off the longest import chain in mathlib.

Estimated changes

Modified src/analysis/calculus/fderiv_measurable.lean

Modified src/measure_theory/function/ae_eq_fun.lean

Modified src/measure_theory/function/ae_eq_of_integral.lean

Modified src/measure_theory/function/lp_space.lean

Created src/measure_theory/function/special_functions/arctan.lean

added theorem measurable.arctan

added theorem real.measurable_arctan

Renamed src/measure_theory/function/special_functions.lean to src/measure_theory/function/special_functions/basic.lean

deleted theorem ae_measurable.inner

deleted theorem measurable.arctan

deleted theorem measurable.inner

deleted theorem real.measurable_arctan

Created src/measure_theory/function/special_functions/inner.lean

added theorem ae_measurable.inner

added theorem measurable.inner

Renamed src/measure_theory/function/strongly_measurable.lean to src/measure_theory/function/strongly_measurable/basic.lean

Created src/measure_theory/function/strongly_measurable/inner.lean

Renamed src/measure_theory/function/strongly_measurable_lp.lean to src/measure_theory/function/strongly_measurable/lp.lean

Modified src/measure_theory/integral/mean_inequalities.lean

Modified test/measurability.lean