Commit 2023-02-02 11:40 da1d134a

View on Github →

feat(analysis/special_functions/pow): strengthen cpow integrability lemmas (#18354) This adds some slightly stronger results about continuity / integrability of x -> x^s for complex s.

Estimated changes

Modified src/analysis/special_functions/integrals.lean

modified theorem integral_cpow

added theorem interval_integral.interval_integrable_cpow'

modified theorem interval_integral.interval_integrable_cpow

Modified src/analysis/special_functions/pow.lean

added theorem complex.continuous_at_of_real_cpow

added theorem complex.continuous_at_of_real_cpow_const

added theorem complex.mul_cpow_of_real_nonneg

modified theorem continuous_at_const_cpow'

modified theorem continuous_at_const_cpow

Modified src/analysis/special_functions/pow_deriv.lean

added theorem has_deriv_at_of_real_cpow