Commit 2023-06-06 13:22 a9359cb3

View on Github →

feat: port Analysis.SpecialFunctions.Pow.Deriv (#4689)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

added theorem Complex.hasFDerivAt_cpow

added theorem Complex.hasStrictDerivAt_const_cpow

added theorem Complex.hasStrictDerivAt_cpow_const

added theorem Complex.hasStrictFDerivAt_cpow'

added theorem Complex.hasStrictFDerivAt_cpow

added theorem ContDiff.rpow

added theorem ContDiff.rpow_const_of_le

added theorem ContDiff.rpow_const_of_ne

added theorem ContDiffAt.rpow

added theorem ContDiffAt.rpow_const_of_le

added theorem ContDiffAt.rpow_const_of_ne

added theorem ContDiffOn.rpow

added theorem ContDiffOn.rpow_const_of_le

added theorem ContDiffOn.rpow_const_of_ne

added theorem ContDiffWithinAt.rpow

added theorem ContDiffWithinAt.rpow_const_of_le

added theorem ContDiffWithinAt.rpow_const_of_ne

added theorem Differentiable.rpow

added theorem Differentiable.rpow_const

added theorem DifferentiableAt.const_cpow

added theorem DifferentiableAt.cpow

added theorem DifferentiableAt.rpow

added theorem DifferentiableAt.rpow_const

added theorem DifferentiableOn.rpow

added theorem DifferentiableOn.rpow_const

added theorem DifferentiableWithinAt.const_cpow

added theorem DifferentiableWithinAt.cpow

added theorem DifferentiableWithinAt.rpow

added theorem DifferentiableWithinAt.rpow_const

added theorem HasDerivAt.const_cpow

added theorem HasDerivAt.cpow

added theorem HasDerivAt.cpow_const

added theorem HasDerivAt.rpow

added theorem HasDerivAt.rpow_const

added theorem HasDerivWithinAt.const_cpow

added theorem HasDerivWithinAt.cpow

added theorem HasDerivWithinAt.cpow_const

added theorem HasDerivWithinAt.rpow

added theorem HasDerivWithinAt.rpow_const

added theorem HasFDerivAt.const_cpow

added theorem HasFDerivAt.const_rpow

added theorem HasFDerivAt.cpow

added theorem HasFDerivAt.rpow

added theorem HasFDerivAt.rpow_const

added theorem HasFDerivWithinAt.const_cpow

added theorem HasFDerivWithinAt.const_rpow

added theorem HasFDerivWithinAt.cpow

added theorem HasFDerivWithinAt.rpow

added theorem HasFDerivWithinAt.rpow_const

added theorem HasStrictDerivAt.const_cpow

added theorem HasStrictDerivAt.cpow_const

added theorem HasStrictDerivAt.rpow

added theorem HasStrictFDerivAt.const_cpow

added theorem HasStrictFDerivAt.const_rpow

added theorem HasStrictFDerivAt.cpow

added theorem HasStrictFDerivAt.rpow

added theorem HasStrictFDerivAt.rpow_const

added theorem Real.contDiffAt_rpow_const

added theorem Real.contDiffAt_rpow_const_of_le

added theorem Real.contDiffAt_rpow_const_of_ne

added theorem Real.contDiffAt_rpow_of_ne

added theorem Real.contDiff_rpow_const_of_le

added theorem Real.deriv_rpow_const'

added theorem Real.deriv_rpow_const

added theorem Real.differentiableAt_rpow_of_ne

added theorem Real.differentiable_rpow_const

added theorem Real.hasDerivAt_rpow_const

added theorem Real.hasStrictDerivAt_const_rpow

added theorem Real.hasStrictDerivAt_const_rpow_of_neg

added theorem Real.hasStrictDerivAt_rpow_const

added theorem Real.hasStrictDerivAt_rpow_const_of_ne

added theorem Real.hasStrictFDerivAt_rpow_of_neg

added theorem Real.hasStrictFDerivAt_rpow_of_pos

added theorem derivWithin_rpow_const

added theorem deriv_rpow_const

added theorem hasDerivAt_of_real_cpow

added theorem tendsto_one_plus_div_pow_exp

added theorem tendsto_one_plus_div_rpow_exp