Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-02 21:57 70ed9dce

View on Github →

chore(analysis/special_functions/trigonometric/basic): move results about derivatives to a new file (#10109) This is part of a refactor of the analysis/special_functions folder, in which I will isolate all lemmas about derivatives. The result will be a definition of Lp spaces that does not import derivatives.

Estimated changes

deleted theorem complex.deriv_cos'
deleted theorem complex.deriv_cos
deleted theorem complex.deriv_cosh
deleted theorem complex.deriv_sin
deleted theorem complex.deriv_sinh
deleted theorem complex.has_deriv_at_cos
deleted theorem complex.has_deriv_at_cosh
deleted theorem complex.has_deriv_at_sin
deleted theorem complex.has_deriv_at_sinh
deleted theorem deriv_ccos
deleted theorem deriv_ccosh
deleted theorem deriv_cos
deleted theorem deriv_cosh
deleted theorem deriv_csin
deleted theorem deriv_csinh
deleted theorem deriv_sin
deleted theorem deriv_sinh
deleted theorem deriv_within_ccos
deleted theorem deriv_within_ccosh
deleted theorem deriv_within_cos
deleted theorem deriv_within_cosh
deleted theorem deriv_within_csin
deleted theorem deriv_within_csinh
deleted theorem deriv_within_sin
deleted theorem deriv_within_sinh
deleted theorem differentiable.ccos
deleted theorem differentiable.ccosh
deleted theorem differentiable.cos
deleted theorem differentiable.cosh
deleted theorem differentiable.csin
deleted theorem differentiable.csinh
deleted theorem differentiable.sin
deleted theorem differentiable.sinh
deleted theorem differentiable_at.ccos
deleted theorem differentiable_at.ccosh
deleted theorem differentiable_at.cos
deleted theorem differentiable_at.cosh
deleted theorem differentiable_at.csin
deleted theorem differentiable_at.csinh
deleted theorem differentiable_at.sin
deleted theorem differentiable_at.sinh
deleted theorem differentiable_on.ccos
deleted theorem differentiable_on.ccosh
deleted theorem differentiable_on.cos
deleted theorem differentiable_on.cosh
deleted theorem differentiable_on.csin
deleted theorem differentiable_on.csinh
deleted theorem differentiable_on.sin
deleted theorem differentiable_on.sinh
deleted theorem fderiv_ccos
deleted theorem fderiv_ccosh
deleted theorem fderiv_cos
deleted theorem fderiv_cosh
deleted theorem fderiv_csin
deleted theorem fderiv_csinh
deleted theorem fderiv_sin
deleted theorem fderiv_sinh
deleted theorem fderiv_within_ccos
deleted theorem fderiv_within_ccosh
deleted theorem fderiv_within_cos
deleted theorem fderiv_within_cosh
deleted theorem fderiv_within_csin
deleted theorem fderiv_within_csinh
deleted theorem fderiv_within_sin
deleted theorem fderiv_within_sinh
deleted theorem has_deriv_at.ccos
deleted theorem has_deriv_at.ccosh
deleted theorem has_deriv_at.cos
deleted theorem has_deriv_at.cosh
deleted theorem has_deriv_at.csin
deleted theorem has_deriv_at.csinh
deleted theorem has_deriv_at.sin
deleted theorem has_deriv_at.sinh
deleted theorem has_deriv_within_at.ccos
deleted theorem has_deriv_within_at.ccosh
deleted theorem has_deriv_within_at.cos
deleted theorem has_deriv_within_at.cosh
deleted theorem has_deriv_within_at.csin
deleted theorem has_deriv_within_at.csinh
deleted theorem has_deriv_within_at.sin
deleted theorem has_deriv_within_at.sinh
deleted theorem has_fderiv_at.ccos
deleted theorem has_fderiv_at.ccosh
deleted theorem has_fderiv_at.cos
deleted theorem has_fderiv_at.cosh
deleted theorem has_fderiv_at.csin
deleted theorem has_fderiv_at.csinh
deleted theorem has_fderiv_at.sin
deleted theorem has_fderiv_at.sinh
deleted theorem has_fderiv_within_at.ccos
deleted theorem has_fderiv_within_at.cos
deleted theorem has_fderiv_within_at.cosh
deleted theorem has_fderiv_within_at.csin
deleted theorem has_fderiv_within_at.sin
deleted theorem has_fderiv_within_at.sinh
deleted theorem has_strict_deriv_at.ccos
deleted theorem has_strict_deriv_at.ccosh
deleted theorem has_strict_deriv_at.cos
deleted theorem has_strict_deriv_at.cosh
deleted theorem has_strict_deriv_at.csin
deleted theorem has_strict_deriv_at.csinh
deleted theorem has_strict_deriv_at.sin
deleted theorem has_strict_deriv_at.sinh
deleted theorem has_strict_fderiv_at.ccos
deleted theorem has_strict_fderiv_at.cos
deleted theorem has_strict_fderiv_at.cosh
deleted theorem has_strict_fderiv_at.csin
deleted theorem has_strict_fderiv_at.sin
deleted theorem has_strict_fderiv_at.sinh
deleted theorem real.deriv_cos'
deleted theorem real.deriv_cos
deleted theorem real.deriv_cosh
deleted theorem real.deriv_sin
deleted theorem real.deriv_sinh
deleted theorem real.differentiable_cos
deleted theorem real.differentiable_cosh
deleted theorem real.differentiable_sin
deleted theorem real.differentiable_sinh
deleted theorem real.has_deriv_at_cos
deleted theorem real.has_deriv_at_cosh
deleted theorem real.has_deriv_at_sin
deleted theorem real.has_deriv_at_sinh
deleted theorem real.sinh_strict_mono
deleted theorem real.times_cont_diff_cos
deleted theorem real.times_cont_diff_cosh
deleted theorem real.times_cont_diff_sin
deleted theorem real.times_cont_diff_sinh
deleted theorem times_cont_diff.ccos
deleted theorem times_cont_diff.ccosh
deleted theorem times_cont_diff.cos
deleted theorem times_cont_diff.cosh
deleted theorem times_cont_diff.csin
deleted theorem times_cont_diff.csinh
deleted theorem times_cont_diff.sin
deleted theorem times_cont_diff.sinh
deleted theorem times_cont_diff_at.ccos
deleted theorem times_cont_diff_at.ccosh
deleted theorem times_cont_diff_at.cos
deleted theorem times_cont_diff_at.cosh
deleted theorem times_cont_diff_at.csin
deleted theorem times_cont_diff_at.csinh
deleted theorem times_cont_diff_at.sin
deleted theorem times_cont_diff_at.sinh
deleted theorem times_cont_diff_on.ccos
deleted theorem times_cont_diff_on.ccosh
deleted theorem times_cont_diff_on.cos
deleted theorem times_cont_diff_on.cosh
deleted theorem times_cont_diff_on.csin
deleted theorem times_cont_diff_on.csinh
deleted theorem times_cont_diff_on.sin
deleted theorem times_cont_diff_on.sinh
added theorem complex.deriv_cos'
added theorem complex.deriv_cos
added theorem complex.deriv_cosh
added theorem complex.deriv_sin
added theorem complex.deriv_sinh
added theorem deriv_ccos
added theorem deriv_ccosh
added theorem deriv_cos
added theorem deriv_cosh
added theorem deriv_csin
added theorem deriv_csinh
added theorem deriv_sin
added theorem deriv_sinh
added theorem deriv_within_ccos
added theorem deriv_within_ccosh
added theorem deriv_within_cos
added theorem deriv_within_cosh
added theorem deriv_within_csin
added theorem deriv_within_csinh
added theorem deriv_within_sin
added theorem deriv_within_sinh
added theorem differentiable.ccos
added theorem differentiable.ccosh
added theorem differentiable.cos
added theorem differentiable.cosh
added theorem differentiable.csin
added theorem differentiable.csinh
added theorem differentiable.sin
added theorem differentiable.sinh
added theorem differentiable_at.ccos
added theorem differentiable_at.cos
added theorem differentiable_at.cosh
added theorem differentiable_at.csin
added theorem differentiable_at.sin
added theorem differentiable_at.sinh
added theorem differentiable_on.ccos
added theorem differentiable_on.cos
added theorem differentiable_on.cosh
added theorem differentiable_on.csin
added theorem differentiable_on.sin
added theorem differentiable_on.sinh
added theorem fderiv_ccos
added theorem fderiv_ccosh
added theorem fderiv_cos
added theorem fderiv_cosh
added theorem fderiv_csin
added theorem fderiv_csinh
added theorem fderiv_sin
added theorem fderiv_sinh
added theorem fderiv_within_ccos
added theorem fderiv_within_ccosh
added theorem fderiv_within_cos
added theorem fderiv_within_cosh
added theorem fderiv_within_csin
added theorem fderiv_within_csinh
added theorem fderiv_within_sin
added theorem fderiv_within_sinh
added theorem has_deriv_at.ccos
added theorem has_deriv_at.ccosh
added theorem has_deriv_at.cos
added theorem has_deriv_at.cosh
added theorem has_deriv_at.csin
added theorem has_deriv_at.csinh
added theorem has_deriv_at.sin
added theorem has_deriv_at.sinh
added theorem has_fderiv_at.ccos
added theorem has_fderiv_at.ccosh
added theorem has_fderiv_at.cos
added theorem has_fderiv_at.cosh
added theorem has_fderiv_at.csin
added theorem has_fderiv_at.csinh
added theorem has_fderiv_at.sin
added theorem has_fderiv_at.sinh
added theorem real.deriv_cos'
added theorem real.deriv_cos
added theorem real.deriv_cosh
added theorem real.deriv_sin
added theorem real.deriv_sinh
added theorem real.has_deriv_at_cos
added theorem real.has_deriv_at_cosh
added theorem real.has_deriv_at_sin
added theorem real.has_deriv_at_sinh
added theorem real.sinh_strict_mono
added theorem times_cont_diff.ccos
added theorem times_cont_diff.ccosh
added theorem times_cont_diff.cos
added theorem times_cont_diff.cosh
added theorem times_cont_diff.csin
added theorem times_cont_diff.csinh
added theorem times_cont_diff.sin
added theorem times_cont_diff.sinh
added theorem times_cont_diff_at.cos
added theorem times_cont_diff_at.sin
added theorem times_cont_diff_on.cos
added theorem times_cont_diff_on.sin