Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-16 15:18 217308c9

View on Github →

feat(analysis): x^y is smooth as a function of (x, y) (#8262)

Estimated changes

Modified src/analysis/calculus/extend_deriv.lean

added theorem has_deriv_at_of_has_deriv_at_of_ne'

Modified src/analysis/convex/specific_functions.lean

Modified src/analysis/special_functions/pow.lean

added theorem complex.has_strict_fderiv_at_cpow'

added theorem continuous.rpow

added theorem continuous.rpow_const

added theorem continuous_at.rpow

added theorem continuous_at.rpow_const

added theorem continuous_on.rpow

added theorem continuous_on.rpow_const

added theorem continuous_within_at.rpow

added theorem continuous_within_at.rpow_const

deleted theorem deriv_rpow

added theorem deriv_rpow_const

deleted theorem deriv_rpow_of_one_le

deleted theorem deriv_within_rpow

added theorem deriv_within_rpow_const

deleted theorem deriv_within_rpow_of_one_le

modified theorem differentiable.rpow

added theorem differentiable.rpow_const

deleted theorem differentiable.rpow_of_one_le

modified theorem differentiable_at.rpow

added theorem differentiable_at.rpow_const

deleted theorem differentiable_at.rpow_of_one_le

modified theorem differentiable_on.rpow

added theorem differentiable_on.rpow_const

deleted theorem differentiable_on.rpow_of_one_le

modified theorem differentiable_within_at.rpow

added theorem differentiable_within_at.rpow_const

deleted theorem differentiable_within_at.rpow_of_one_le

added theorem filter.tendsto.rpow

added theorem filter.tendsto.rpow_const

modified theorem has_deriv_at.rpow

added theorem has_deriv_at.rpow_const

deleted theorem has_deriv_at.rpow_of_one_le

modified theorem has_deriv_within_at.rpow

added theorem has_deriv_within_at.rpow_const

deleted theorem has_deriv_within_at.rpow_of_one_le

added theorem has_fderiv_at.const_rpow

added theorem has_fderiv_at.rpow

added theorem has_fderiv_at.rpow_const

added theorem has_fderiv_within_at.const_rpow

added theorem has_fderiv_within_at.rpow

added theorem has_fderiv_within_at.rpow_const

added theorem has_strict_deriv_at.rpow

added theorem has_strict_fderiv_at.const_rpow

added theorem has_strict_fderiv_at.rpow

added theorem has_strict_fderiv_at.rpow_const

added theorem real.abs_rpow_le_exp_log_mul

modified theorem real.continuous_at_rpow

added theorem real.continuous_at_rpow_of_ne

deleted theorem real.continuous_at_rpow_of_ne_zero

modified theorem real.continuous_at_rpow_of_pos

deleted theorem real.continuous_rpow

deleted theorem real.continuous_rpow_aux1

deleted theorem real.continuous_rpow_aux2

deleted theorem real.continuous_rpow_aux3

deleted theorem real.continuous_rpow_of_ne_zero

deleted theorem real.continuous_rpow_of_pos

added theorem real.deriv_rpow_const'

added theorem real.deriv_rpow_const

added theorem real.differentiable_at_rpow_of_ne

added theorem real.differentiable_rpow_const

deleted theorem real.has_deriv_at_rpow

added theorem real.has_deriv_at_rpow_const

deleted theorem real.has_deriv_at_rpow_of_neg

deleted theorem real.has_deriv_at_rpow_of_one_le

deleted theorem real.has_deriv_at_rpow_of_pos

deleted theorem real.has_deriv_at_rpow_zero_of_one_le

added theorem real.has_strict_deriv_at_const_rpow

added theorem real.has_strict_deriv_at_const_rpow_of_neg

added theorem real.has_strict_deriv_at_rpow_const

added theorem real.has_strict_deriv_at_rpow_const_of_ne

added theorem real.has_strict_fderiv_at_rpow_of_neg

added theorem real.has_strict_fderiv_at_rpow_of_pos

added theorem real.rpow_add_int

added theorem real.rpow_add_nat

added theorem real.rpow_add_one

added theorem real.rpow_sub_int

added theorem real.rpow_sub_nat

added theorem real.rpow_sub_one

added theorem real.times_cont_diff_at_rpow_const

added theorem real.times_cont_diff_at_rpow_const_of_le

added theorem real.times_cont_diff_at_rpow_const_of_ne

added theorem real.times_cont_diff_at_rpow_of_ne

added theorem real.times_cont_diff_rpow_const_of_le

added theorem times_cont_diff.rpow

added theorem times_cont_diff.rpow_const_of_le

added theorem times_cont_diff.rpow_const_of_ne

added theorem times_cont_diff_at.rpow

added theorem times_cont_diff_at.rpow_const_of_le

added theorem times_cont_diff_at.rpow_const_of_ne

added theorem times_cont_diff_on.rpow

added theorem times_cont_diff_on.rpow_const_of_le

added theorem times_cont_diff_on.rpow_const_of_ne

added theorem times_cont_diff_within_at.rpow

added theorem times_cont_diff_within_at.rpow_const_of_le

added theorem times_cont_diff_within_at.rpow_const_of_ne