Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-13 10:27 ce86d33b

View on Github →

feat(analysis/calculus/(f)deriv): differentiability of a finite sum of functions (#2657) We show that, if each f i is differentiable, then λ y, ∑ i in s, f i y is also differentiable when s is a finset, and give the lemmas around this for fderiv and deriv.

Estimated changes

added theorem asymptotics.is_O.sum
modified theorem asymptotics.is_O_with_zero
modified theorem asymptotics.is_O_zero
added theorem asymptotics.is_o.sum
added theorem deriv_div_const
added theorem deriv_sum
added theorem deriv_within_div_const
added theorem deriv_within_sum
added theorem has_deriv_at.sum
added theorem differentiable.sum
added theorem differentiable_at.sum
added theorem differentiable_on.sum
added theorem fderiv_sum
added theorem fderiv_within_sum
added theorem has_fderiv_at.sum