Commit 2022-10-27 07:38 1a249186

View on Github →

feat(analysis/calculus/uniform_limits_deriv): pointwise convergence out of derivative convergence on a preconnected set (#17123) Also cleanup the file calculus/uniform_limits_deriv by removing unnecessary typeclass assumptions, fixing lemma names and docstrings, and replacing convergence assumptions by Cauchyness assumption when the limit is not relevant.

Estimated changes

Modified src/analysis/calculus/uniform_limits_deriv.lean

added theorem cauchy_map_of_uniform_cauchy_seq_on_fderiv

modified theorem has_deriv_at_of_tendsto_uniformly

modified theorem has_deriv_at_of_tendsto_uniformly_on

modified theorem has_deriv_at_of_tendsto_uniformly_on_filter

modified theorem has_fderiv_at_of_tendsto_uniformly

modified theorem has_fderiv_at_of_tendsto_uniformly_on

modified theorem has_fderiv_at_of_tendsto_uniformly_on_filter

added theorem uniform_cauchy_seq_on_ball_of_deriv

added theorem uniform_cauchy_seq_on_ball_of_fderiv

deleted theorem uniform_cauchy_seq_on_ball_of_tendsto_uniformly_on_ball_deriv

deleted theorem uniform_cauchy_seq_on_ball_of_tendsto_uniformly_on_ball_fderiv

added theorem uniform_cauchy_seq_on_filter_of_deriv

added theorem uniform_cauchy_seq_on_filter_of_fderiv

deleted theorem uniform_cauchy_seq_on_filter_of_tendsto_uniformly_on_filter_deriv

deleted theorem uniform_cauchy_seq_on_filter_of_tendsto_uniformly_on_filter_fderiv

Modified src/topology/uniform_space/uniform_convergence.lean

added theorem uniform_cauchy_seq_on.cauchy_map