Commit 2023-06-09 14:11 87c0e820

View on Github →

feat: port Analysis.Complex.LocallyUniformLimit (#4906)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/LocallyUniformLimit.lean

added theorem Complex.cderiv_eq_deriv

added theorem Complex.cderiv_sub

added theorem Complex.differentiableOn_tsum_of_summable_norm

added theorem Complex.exists_cthickening_tendstoUniformlyOn

added theorem Complex.hasSum_deriv_of_summable_norm

added theorem Complex.norm_cderiv_le

added theorem Complex.norm_cderiv_lt

added theorem Complex.norm_cderiv_sub_lt

added theorem Complex.tendstoUniformlyOn_deriv_of_cthickening_subset

added theorem TendstoLocallyUniformlyOn.deriv

added theorem TendstoLocallyUniformlyOn.differentiableOn

added theorem TendstoUniformlyOn.cderiv