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