Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-28 10:49 ef5c1d50

View on Github →

feat(analysis/special_functions/pow): smoothness of complex.cpow (#6447)

x ^ y is smooth in both variables at (x, y), if 0 < re x or im x ≠ 0;
x ^ y is smooth in y if x ≠ 0 or y ≠ 0.

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem complex.cpow_def_of_ne_zero

added theorem complex.cpow_sub

added theorem complex.has_fderiv_at_cpow

added theorem complex.has_strict_deriv_at_const_cpow

added theorem complex.has_strict_deriv_at_cpow_const

added theorem complex.has_strict_fderiv_at_cpow

added theorem continuous.const_cpow

added theorem continuous.cpow

added theorem continuous_at.const_cpow

added theorem continuous_at.cpow

added theorem continuous_on.const_cpow

added theorem continuous_on.cpow

added theorem continuous_within_at.const_cpow

added theorem continuous_within_at.cpow

added theorem differentiable_at.const_cpow

added theorem differentiable_at.cpow

added theorem differentiable_within_at.const_cpow

added theorem differentiable_within_at.cpow

added theorem filter.tendsto.const_cpow

added theorem filter.tendsto.cpow

added theorem has_deriv_at.const_cpow

added theorem has_deriv_at.cpow

added theorem has_deriv_at.cpow_const

added theorem has_deriv_within_at.const_cpow

added theorem has_deriv_within_at.cpow

added theorem has_deriv_within_at.cpow_const

added theorem has_fderiv_at.const_cpow

added theorem has_fderiv_at.cpow

added theorem has_fderiv_within_at.const_cpow

added theorem has_fderiv_within_at.cpow

added theorem has_strict_deriv_at.const_cpow

added theorem has_strict_deriv_at.cpow

added theorem has_strict_deriv_at.cpow_const

added theorem has_strict_fderiv_at.const_cpow

added theorem has_strict_fderiv_at.cpow

modified theorem measurable.cpow

Modified src/analysis/special_functions/trigonometric.lean

added theorem complex.log_im_le_pi

added theorem complex.neg_pi_lt_log_im

added theorem real.cos_sub_pi