From 5aabd4ed48ee72fd693b8ae1980712f6ef14e4f1 Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Sat, 16 Dec 2023 00:27:09 +0000 Subject: [PATCH] feat: Add `congr_deriv` lemmas mirroring `congr_fderiv` (#9065) Add convenience lemmas * `HasStrictDerivAt.congr_deriv` * `HasDerivAt.congr_deriv` * `HasDerivWithinAt.congr_deriv` These mirror the already existing * `HasStrictFDerivAt.congr_fderiv` * `HasFDerivAt.congr_fderiv` * `HasFDerivWithinAt.congr_fderiv` --- Mathlib/Analysis/Calculus/Deriv/Basic.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Mathlib/Analysis/Calculus/Deriv/Basic.lean b/Mathlib/Analysis/Calculus/Deriv/Basic.lean index 3b25240ada6f86..8577837699cf2c 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Basic.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Basic.lean @@ -614,6 +614,17 @@ theorem Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem (h₁ : f₁ =ᶠ[𝓝[s ⟨fun h' ↦ h'.congr_of_eventuallyEq_of_mem h₁.symm hx, fun h' ↦ h'.congr_of_eventuallyEq_of_mem h₁ hx⟩ +theorem HasStrictDerivAt.congr_deriv (h : HasStrictDerivAt f f' x) (h' : f' = g') : + HasStrictDerivAt f g' x := + h.congr_fderiv <| congr_arg _ h' + +theorem HasDerivAt.congr_deriv (h : HasDerivAt f f' x) (h' : f' = g') : HasDerivAt f g' x := + HasFDerivAt.congr_fderiv h <| congr_arg _ h' + +theorem HasDerivWithinAt.congr_deriv (h : HasDerivWithinAt f f' s x) (h' : f' = g') : + HasDerivWithinAt f g' s x := + HasFDerivWithinAt.congr_fderiv h <| congr_arg _ h' + theorem HasDerivAt.congr_of_eventuallyEq (h : HasDerivAt f f' x) (h₁ : f₁ =ᶠ[𝓝 x] f) : HasDerivAt f₁ f' x := HasDerivAtFilter.congr_of_eventuallyEq h h₁ (mem_of_mem_nhds h₁ : _)