Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-20 17:21 fae00c7c

View on Github →

chore(analysis/special_functions): move measurability statements to measure_theory folder (#8006) Make sure that measure theory is not imported in basic files defining trigonometric functions and real powers. The measurability of these functions is postponed to a new file measure_theory.special_functions.

Estimated changes

deleted theorem ae_measurable.inner
deleted theorem measurable.inner
deleted theorem complex.measurable_exp
deleted theorem complex.measurable_im
deleted theorem complex.measurable_re
deleted theorem measurable.cexp
deleted theorem measurable.exp
deleted theorem measurable.log
deleted theorem real.measurable_exp
deleted theorem real.measurable_log
deleted theorem measurable.sqrt
deleted theorem complex.measurable_arg
deleted theorem complex.measurable_cos
deleted theorem complex.measurable_cosh
deleted theorem complex.measurable_log
deleted theorem complex.measurable_sin
deleted theorem complex.measurable_sinh
deleted theorem measurable.arctan
deleted theorem measurable.carg
deleted theorem measurable.ccos
deleted theorem measurable.ccosh
deleted theorem measurable.clog
deleted theorem measurable.cos
deleted theorem measurable.cosh
deleted theorem measurable.csin
deleted theorem measurable.csinh
deleted theorem measurable.sin
deleted theorem measurable.sinh
deleted theorem real.measurable_arccos
deleted theorem real.measurable_arcsin
deleted theorem real.measurable_arctan
deleted theorem real.measurable_cos
deleted theorem real.measurable_cosh
deleted theorem real.measurable_sin
deleted theorem real.measurable_sinh
added theorem ae_measurable.inner
added theorem complex.measurable_arg
added theorem complex.measurable_cos
added theorem complex.measurable_exp
added theorem complex.measurable_im
added theorem complex.measurable_log
added theorem complex.measurable_re
added theorem complex.measurable_sin
added theorem measurable.arctan
added theorem measurable.carg
added theorem measurable.ccos
added theorem measurable.ccosh
added theorem measurable.cexp
added theorem measurable.clog
added theorem measurable.cos
added theorem measurable.cosh
added theorem measurable.csin
added theorem measurable.csinh
added theorem measurable.exp
added theorem measurable.inner
added theorem measurable.log
added theorem measurable.sin
added theorem measurable.sinh
added theorem measurable.sqrt
added theorem real.measurable_arccos
added theorem real.measurable_arcsin
added theorem real.measurable_arctan
added theorem real.measurable_cos
added theorem real.measurable_cosh
added theorem real.measurable_exp
added theorem real.measurable_log
added theorem real.measurable_sin
added theorem real.measurable_sinh