Commit 2022-11-22 12:28 563bbc0c

View on Github →

feat(analysis/calculus): smoothness of series of functions (#17110) We show that infinite series of functions are continuous/differentiable/smooth under suitable summability assumptions.

Estimated changes

Modified src/analysis/calculus/cont_diff.lean

added theorem cont_diff_iff_forall_nat_le

added theorem fderiv_iterated_fderiv

added theorem has_compact_support.iterated_fderiv

Created src/analysis/calculus/series.lean

added theorem cont_diff_tsum

added theorem cont_diff_tsum_of_eventually

added theorem continuous_on_tsum

added theorem continuous_tsum

added theorem differentiable_tsum

added theorem fderiv_tsum

added theorem fderiv_tsum_apply

added theorem has_fderiv_at_tsum

added theorem has_fderiv_at_tsum_of_is_preconnected

added theorem iterated_fderiv_tsum

added theorem iterated_fderiv_tsum_apply

added theorem summable_of_summable_has_fderiv_at

added theorem summable_of_summable_has_fderiv_at_of_is_preconnected

added theorem tendsto_uniformly_on_tsum

added theorem tendsto_uniformly_on_tsum_nat

added theorem tendsto_uniformly_tsum

added theorem tendsto_uniformly_tsum_nat

Modified src/topology/algebra/infinite_sum.lean

added theorem sum_add_tsum_subtype_compl

added theorem tsum_subtype_add_tsum_subtype_compl

Modified src/topology/instances/ennreal.lean

added theorem summable.to_nnreal