Commit 2024-01-07 18:13 d274b397

View on Github →

feat: estimates for the complex logarithm (#9270) This PR adds estimates for the difference of the complex logarithm log (1+z) and its nth Taylor polynomial in terms of ‖z‖ when ‖z‖ < 1. See this thread on Zulip.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

added theorem Complex.continuousOn_one_add_mul_inv

added theorem Complex.hasDerivAt_logTaylor

added theorem Complex.hasDerivAt_log_sub_logTaylor

added theorem Complex.hasSum_taylorSeries_log

added theorem Complex.hasSum_taylorSeries_neg_log

added theorem Complex.integrable_pow_mul_norm_one_add_mul_inv

added def Complex.logTaylor

added theorem Complex.logTaylor_at_zero

added theorem Complex.logTaylor_succ

added theorem Complex.logTaylor_zero

added theorem Complex.log_eq_integral

added theorem Complex.log_inv_eq_integral

added theorem Complex.norm_log_one_add_sub_self_le

added theorem Complex.norm_log_one_sub_inv_add_logTaylor_neg_le

added theorem Complex.norm_log_one_sub_inv_sub_self_le

added theorem Complex.norm_log_sub_logTaylor_le

added theorem Complex.norm_one_add_mul_inv_le

Modified Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean

added theorem Complex.differentiableAt_log

added theorem Complex.hasDerivAt_log