Commit 2020-07-31 17:41 396a764f

View on Github →

feat(analysis/calculus/fderiv): inversion is differentiable (#3510) At an invertible element x of a complete normed algebra, the inversion operation of the algebra is Fréchet-differentiable, with derivative λ t, - x⁻¹ * t * x⁻¹.

Estimated changes

Modified src/algebra/ring/basic.lean

added theorem ring.inverse_unit

Modified src/analysis/asymptotics.lean

added theorem asymptotics.is_o_id_const

Modified src/analysis/calculus/fderiv.lean

added theorem differentiable_at_inverse

added theorem fderiv_inverse

added theorem has_fderiv_at_inverse

Modified src/analysis/normed_space/basic.lean

modified theorem summable_of_norm_bounded

added theorem tsum_of_norm_bounded

Modified src/analysis/normed_space/units.lean

added theorem normed_ring.inverse_add

added theorem normed_ring.inverse_add_norm

added theorem normed_ring.inverse_add_norm_diff_first_order

added theorem normed_ring.inverse_add_norm_diff_nth_order

added theorem normed_ring.inverse_add_norm_diff_second_order

added theorem normed_ring.inverse_add_nth_order

added theorem normed_ring.inverse_continuous_at

added theorem normed_ring.inverse_one_sub

added theorem normed_ring.inverse_one_sub_norm

added theorem normed_ring.inverse_one_sub_nth_order

modified def units.add

modified theorem units.add_coe

modified theorem units.one_sub_coe

modified def units.unit_of_nearby

modified theorem units.unit_of_nearby_coe

Modified src/analysis/specific_limits.lean

added theorem normed_ring.tsum_geometric_of_norm_lt_1

Modified src/topology/algebra/ring.lean

added theorem mul_left_continuous

added theorem mul_right_continuous