Commit 2020-05-15 21:05 f5f7a3cf

View on Github →

feat(analysis/special_functions/exp_log): power series for log around 1 (#2646) This PR adds the power series expansion for the real logarithm around 1, in the form

has_sum (λ (n : ℕ), x ^ (n + 1) / (n + 1)) (-log (1 - x))

Estimated changes

Modified src/algebra/ordered_field.lean

added theorem div_le_div

Modified src/analysis/calculus/extend_deriv.lean

Modified src/analysis/calculus/mean_value.lean

modified theorem convex.norm_image_sub_le_of_norm_deriv_le

added theorem convex.norm_image_sub_le_of_norm_deriv_within_le

added theorem convex.norm_image_sub_le_of_norm_fderiv_le

added theorem convex.norm_image_sub_le_of_norm_fderiv_within_le

added theorem convex.norm_image_sub_le_of_norm_has_deriv_within_le

added theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.norm_id_field'

added theorem continuous_linear_map.norm_id_field

Modified src/analysis/special_functions/exp_log.lean

added theorem real.abs_log_sub_add_sum_range_le

added theorem real.has_sum_pow_div_log_of_abs_lt_1