Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-24 02:31 3a69562d

View on Github →

feat(analysis/calculus): drop unneeded assumptions (#19045)

Prove more precise congruence lemmas for derivatives. In particular, adding or removing a single point from s doesn't change anything about derivatives within s.
Drop has_fderiv_within_at.antimono and has_deriv_within_at.antimono, use stronger *.mono_of_mem lemmas instead.
Prove some equalities about (f)deriv_within by using simp instead of slit_ifs: if has_fderiv_within_at f f' s x ↔ has_fderiv_within_at g g' t y, then fderiv_within f s x = fderiv_within g t y.

Estimated changes

Modified src/analysis/calculus/cont_diff.lean

Modified src/analysis/calculus/cont_diff_def.lean

added theorem cont_diff_within_at.cont_diff_on'

added theorem cont_diff_within_at.differentiable_within_at_iterated_fderiv_within

added theorem filter.eventually_eq.iterated_fderiv_within'

added theorem filter.eventually_eq.iterated_fderiv_within_eq

modified theorem iterated_fderiv_within_congr

added theorem iterated_fderiv_within_congr_set

added theorem iterated_fderiv_within_eventually_congr_set'

added theorem iterated_fderiv_within_eventually_congr_set

modified theorem iterated_fderiv_within_inter'

modified theorem iterated_fderiv_within_inter

modified theorem iterated_fderiv_within_inter_open

Modified src/analysis/calculus/deriv.lean

modified theorem deriv_within_congr

added theorem deriv_within_congr_set'

added theorem deriv_within_congr_set

modified theorem deriv_within_inter

added theorem deriv_within_of_mem

modified theorem filter.eventually_eq.deriv_within_eq

added theorem has_deriv_within_at.mono_of_mem

added theorem has_deriv_within_at_congr_set'

modified theorem has_deriv_within_at_congr_set

Modified src/analysis/calculus/fderiv/basic.lean

deleted theorem differentiable_within_at.antimono

added theorem differentiable_within_at_congr_set'

added theorem differentiable_within_at_congr_set

modified theorem fderiv_within_congr'

modified theorem fderiv_within_congr

added theorem fderiv_within_congr_set'

added theorem fderiv_within_congr_set

added theorem fderiv_within_eventually_congr_set'

added theorem fderiv_within_eventually_congr_set

modified theorem fderiv_within_inter

added theorem fderiv_within_of_mem

deleted theorem fderiv_within_subset'

modified theorem filter.eventually_eq.fderiv_eq

added theorem filter.eventually_eq.fderiv_within'

modified theorem filter.eventually_eq.fderiv_within_eq

modified theorem filter.eventually_eq.fderiv_within_eq_nhds

deleted theorem has_fderiv_within_at.antimono

modified theorem has_fderiv_within_at.congr'

modified theorem has_fderiv_within_at.congr

modified theorem has_fderiv_within_at.congr_mono

modified theorem has_fderiv_within_at.insert

added theorem has_fderiv_within_at_congr_set'

added theorem has_fderiv_within_at_congr_set

added theorem has_fderiv_within_at_diff_singleton

modified theorem has_fderiv_within_at_insert

added theorem tsupport_fderiv_subset

Modified src/analysis/calculus/iterated_deriv.lean

added theorem cont_diff_within_at.differentiable_within_at_iterated_deriv_within

modified theorem iterated_deriv_within_one

Modified src/analysis/calculus/taylor.lean

modified theorem has_deriv_within_at_taylor_coeff_within

Modified src/geometry/manifold/cont_mdiff_mfderiv.lean

Modified src/geometry/manifold/mfderiv.lean

modified theorem mfderiv_within_inter

Modified src/geometry/manifold/vector_bundle/tangent.lean