From d32e895b45d5954d96c5e36555db2d2c9803aff0 Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Thu, 14 Dec 2023 17:12:47 -0800 Subject: [PATCH 1/2] congr_deriv --- 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 3b25240ada6f8..2c9c2b6137886 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' ▸ h + +theorem HasDerivAt.congr_deriv (h : HasDerivAt f f' x) (h' : f' = g') : HasDerivAt f g' x := + h' ▸ h + +theorem HasDerivWithinAt.congr_deriv (h : HasDerivWithinAt f f' s x) (h' : f' = g') : + HasDerivWithinAt f g' s x := + h' ▸ 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₁ : _) From 21df766c3e92396d15ae06a75240dee7b3f86ec4 Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Fri, 15 Dec 2023 12:57:28 -0800 Subject: [PATCH 2/2] Update Mathlib/Analysis/Calculus/Deriv/Basic.lean Co-authored-by: Eric Wieser --- Mathlib/Analysis/Calculus/Deriv/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/Calculus/Deriv/Basic.lean b/Mathlib/Analysis/Calculus/Deriv/Basic.lean index 2c9c2b6137886..8577837699cf2 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Basic.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Basic.lean @@ -616,14 +616,14 @@ theorem Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem (h₁ : f₁ =ᶠ[𝓝[s theorem HasStrictDerivAt.congr_deriv (h : HasStrictDerivAt f f' x) (h' : f' = g') : HasStrictDerivAt f g' x := - h' ▸ h + h.congr_fderiv <| congr_arg _ h' theorem HasDerivAt.congr_deriv (h : HasDerivAt f f' x) (h' : f' = g') : HasDerivAt f g' x := - h' ▸ h + 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 := - h' ▸ h + 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 :=