Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-29 12:11 fa09f493

View on Github →

feat(analysis/special_functions/*): prove that exp etc are measurable (#4314) The modifications in measure_theory/borel_space are a part of the proof of measurability of x^y, x : ennreal, y : ℝ, but this proof depends on a refactoring of arcsin I'm going to PR soon.

Estimated changes

added theorem complex.measurable_exp
added theorem measurable.cexp
added theorem measurable.exp
added theorem measurable.log
modified theorem real.continuous_log'
added theorem real.measurable_exp
added theorem real.measurable_log
added theorem complex.measurable_cos
added theorem complex.measurable_sin
added theorem measurable.ccos
added theorem measurable.ccosh
added theorem measurable.cos
added theorem measurable.cosh
added theorem measurable.csin
added theorem measurable.csinh
added theorem measurable.sin
added theorem measurable.sinh
added theorem real.measurable_cos
added theorem real.measurable_cosh
added theorem real.measurable_sin
added theorem real.measurable_sinh
added theorem ennreal.measurable_mul
added theorem ennreal.measurable_sub
modified theorem measurable.ennreal_mul
modified theorem measurable.ennreal_sub
deleted theorem measurable_to_nnreal
modified theorem measurable_const