Commit 2025-01-20 16:09 00664149

feat(Analysis/Pow/Deriv): add some results about differentiability of cpow (#19944)

• Add several results that exists for rpow but not for cpow:

• • DifferentiableAt.cpow_const, DifferentiableWithinAt.cpow_const and DifferentiableOn.cpow_const about the differentiability of z ↦ (f z) ^ c
• • Complex.deriv_cpow_const and deriv_cpow_const for computing deriv

• Add also an alternate version of hasDerivAt_ofReal_cpow on the differentiability of fun y : ℝ => (y : ℂ) ^ c and the corresponding DifferentiableAt and deriv results that follow.
• Add the equivalent for fun y : ℝ => (y : ℂ) ^ c of isTheta_deriv_rpow_const_atTop and isBigO_deriv_rpow_const_atTop This PR doesn't add new maths since all the results proved are direct consequences of existing results.