Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-05 16:16 1b2048d7

View on Github →

feat(analysis/special_functions/pow): rpow is differentiable (#2930) Differentiability of the real power function x ↦ x^p. Also register the lemmas about the composition with a function to make sure that the simplifier can handle automatically the differentiability of x ↦ (f x)^p and more complicated expressions involving powers.

Estimated changes

added theorem real.exp_log_of_neg
added theorem complex.cpow_neg_one
added theorem deriv_rpow
added theorem deriv_rpow_of_one_le
added theorem deriv_sqrt
added theorem deriv_within_rpow
added theorem deriv_within_sqrt
added theorem differentiable.rpow
added theorem differentiable.sqrt
added theorem differentiable_at.rpow
added theorem differentiable_at.sqrt
added theorem differentiable_on.rpow
added theorem differentiable_on.sqrt
added theorem has_deriv_at.rpow
added theorem has_deriv_at.sqrt
added theorem real.has_deriv_at_rpow
added theorem real.le_rpow_add
added theorem real.rpow_add'
modified theorem real.rpow_add
added theorem real.rpow_neg_one
added theorem real.zero_rpow_le_one
added theorem real.zero_rpow_nonneg