From 4538449682aabfba3b078ff2296c74712aa741d9 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 25 May 2023 21:14:33 +0000 Subject: [PATCH] feat: weaken assumptions in lemmas about `fderivWithin` (#4330) This is a partial forward-port of leanprover-community/mathlib#19045. I only forward-ported 1 file that was already merged into `master`. I'll do some git history rewrites in pending PRs instead. --- Mathlib/Analysis/Calculus/FDeriv/Basic.lean | 208 +++++++++++--------- 1 file changed, 116 insertions(+), 92 deletions(-) diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean index 2be2b4e551c17..4485daf6e1bbb 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Sébastien Gouëzel, Yury Kudryashov ! This file was ported from Lean 3 source module analysis.calculus.fderiv.basic -! leanprover-community/mathlib commit e3fb84046afd187b710170887195d50bada934ee +! leanprover-community/mathlib commit 3a69562db5a458db8322b190ec8d9a8bbd8a5b14 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -391,13 +391,13 @@ theorem hasFDerivWithinAt_univ : HasFDerivWithinAt f f' univ x ↔ HasFDerivAt f alias hasFDerivWithinAt_univ ↔ HasFDerivWithinAt.hasFDerivAt_of_univ _ #align has_fderiv_within_at.has_fderiv_at_of_univ HasFDerivWithinAt.hasFDerivAt_of_univ -theorem hasFDerivWithinAt_insert {y : E} {g' : E →L[𝕜] F} : - HasFDerivWithinAt g g' (insert y s) x ↔ HasFDerivWithinAt g g' s x := by +theorem hasFDerivWithinAt_insert {y : E} : + HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x := by rcases eq_or_ne x y with (rfl | h) · simp_rw [HasFDerivWithinAt, HasFDerivAtFilter] apply Asymptotics.isLittleO_insert - simp only [sub_self, g'.map_zero] - refine' ⟨fun h => h.mono <| subset_insert y s, fun hg => hg.mono_of_mem _⟩ + simp only [sub_self, map_zero] + refine' ⟨fun h => h.mono <| subset_insert y s, fun hf => hf.mono_of_mem _⟩ simp_rw [nhdsWithin_insert_of_ne h, self_mem_nhdsWithin] #align has_fderiv_within_at_insert hasFDerivWithinAt_insert @@ -405,11 +405,16 @@ alias hasFDerivWithinAt_insert ↔ HasFDerivWithinAt.of_insert HasFDerivWithinAt #align has_fderiv_within_at.of_insert HasFDerivWithinAt.of_insert #align has_fderiv_within_at.insert' HasFDerivWithinAt.insert' -theorem HasFDerivWithinAt.insert {g' : E →L[𝕜] F} (h : HasFDerivWithinAt g g' s x) : +theorem HasFDerivWithinAt.insert (h : HasFDerivWithinAt g g' s x) : HasFDerivWithinAt g g' (insert x s) x := h.insert' #align has_fderiv_within_at.insert HasFDerivWithinAt.insert +theorem hasFDerivWithinAt_diff_singleton (y : E) : + HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x := by + rw [← hasFDerivWithinAt_insert, insert_diff_singleton, hasFDerivWithinAt_insert] +#align has_fderiv_within_at_diff_singleton hasFDerivWithinAt_diff_singleton + theorem HasStrictFDerivAt.isBigO_sub (hf : HasStrictFDerivAt f f' x) : (fun p : E × E => f p.1 - f p.2) =O[𝓝 (x, x)] fun p : E × E => p.1 - p.2 := hf.isBigO.congr_of_sub.2 (f'.isBigO_comp _ _) @@ -568,7 +573,7 @@ theorem DifferentiableWithinAt.mono (h : DifferentiableWithinAt 𝕜 f t x) (st #align differentiable_within_at.mono DifferentiableWithinAt.mono theorem DifferentiableWithinAt.mono_of_mem (h : DifferentiableWithinAt 𝕜 f s x) {t : Set E} - (hst : s ∈ nhdsWithin x t) : DifferentiableWithinAt 𝕜 f t x := + (hst : s ∈ 𝓝[t] x) : DifferentiableWithinAt 𝕜 f t x := (h.hasFDerivWithinAt.mono_of_mem hst).differentiableWithinAt #align differentiable_within_at.mono_of_mem DifferentiableWithinAt.mono_of_mem @@ -578,28 +583,14 @@ theorem differentiableWithinAt_univ : DifferentiableWithinAt 𝕜 f univ x ↔ D theorem differentiableWithinAt_inter (ht : t ∈ 𝓝 x) : DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x := by - simp only [DifferentiableWithinAt, HasFDerivWithinAt, HasFDerivAtFilter, - nhdsWithin_restrict' s ht] + simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter ht] #align differentiable_within_at_inter differentiableWithinAt_inter theorem differentiableWithinAt_inter' (ht : t ∈ 𝓝[s] x) : DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x := by - simp only [DifferentiableWithinAt, HasFDerivWithinAt, HasFDerivAtFilter, - nhdsWithin_restrict'' s ht] + simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter' ht] #align differentiable_within_at_inter' differentiableWithinAt_inter' -theorem DifferentiableWithinAt.antimono (h : DifferentiableWithinAt 𝕜 f s x) (hst : s ⊆ t) - (hx : s ∈ 𝓝[t] x) : DifferentiableWithinAt 𝕜 f t x := by - rwa [← differentiableWithinAt_inter' hx, inter_eq_self_of_subset_right hst] -#align differentiable_within_at.antimono DifferentiableWithinAt.antimono - -theorem HasFDerivWithinAt.antimono (h : HasFDerivWithinAt f f' s x) (hst : s ⊆ t) - (hs : UniqueDiffWithinAt 𝕜 s x) (hx : s ∈ 𝓝[t] x) : HasFDerivWithinAt f f' t x := by - have h' : HasFDerivWithinAt f _ t x := - (h.differentiableWithinAt.antimono hst hx).hasFDerivWithinAt - rwa [hs.eq h (h'.mono hst)] -#align has_fderiv_within_at.antimono HasFDerivWithinAt.antimono - theorem DifferentiableAt.differentiableWithinAt (h : DifferentiableAt 𝕜 f x) : DifferentiableWithinAt 𝕜 f s x := (differentiableWithinAt_univ.2 h).mono (subset_univ _) @@ -635,45 +626,31 @@ theorem differentiableOn_of_locally_differentiableOn exact (differentiableWithinAt_inter (IsOpen.mem_nhds t_open xt)).1 (ht x ⟨xs, xt⟩) #align differentiable_on_of_locally_differentiable_on differentiableOn_of_locally_differentiableOn +theorem fderivWithin_of_mem (st : t ∈ 𝓝[s] x) (ht : UniqueDiffWithinAt 𝕜 s x) + (h : DifferentiableWithinAt 𝕜 f t x) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x := + ((DifferentiableWithinAt.hasFDerivWithinAt h).mono_of_mem st).fderivWithin ht +#align fderiv_within_of_mem fderivWithin_of_mem + theorem fderivWithin_subset (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f t x) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x := - ((DifferentiableWithinAt.hasFDerivWithinAt h).mono st).fderivWithin ht + fderivWithin_of_mem (nhdsWithin_mono _ st self_mem_nhdsWithin) ht h #align fderiv_within_subset fderivWithin_subset -theorem fderivWithin_subset' (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x) (hx : s ∈ 𝓝[t] x) - (h : DifferentiableWithinAt 𝕜 f s x) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x := - fderivWithin_subset st ht (h.antimono st hx) -#align fderiv_within_subset' fderivWithin_subset' - -@[simp] -theorem fderivWithin_univ : fderivWithin 𝕜 f univ = fderiv 𝕜 f := by - ext x : 1 - by_cases h : DifferentiableAt 𝕜 f x - · apply HasFDerivWithinAt.fderivWithin _ uniqueDiffWithinAt_univ - rw [hasFDerivWithinAt_univ] - apply h.hasFDerivAt - · have : ¬DifferentiableWithinAt 𝕜 f univ x := by rwa [differentiableWithinAt_univ] - rw [fderiv_zero_of_not_differentiableAt h, fderivWithin_zero_of_not_differentiableWithinAt this] -#align fderiv_within_univ fderivWithin_univ - -theorem fderivWithin_inter (ht : t ∈ 𝓝 x) (hs : UniqueDiffWithinAt 𝕜 s x) : - fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x := by - by_cases h : DifferentiableWithinAt 𝕜 f (s ∩ t) x - · apply fderivWithin_subset (inter_subset_left _ _) _ ((differentiableWithinAt_inter ht).1 h) - apply hs.inter ht - · have : ¬DifferentiableWithinAt 𝕜 f s x := by rwa [← differentiableWithinAt_inter ht] - rw [fderivWithin_zero_of_not_differentiableWithinAt h, - fderivWithin_zero_of_not_differentiableWithinAt this] +theorem fderivWithin_inter (ht : t ∈ 𝓝 x) : fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x := by + simp only [fderivWithin, hasFDerivWithinAt_inter ht] #align fderiv_within_inter fderivWithin_inter theorem fderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x := by - have : s = univ ∩ s := by simp only [univ_inter] - rw [this, ← fderivWithin_univ] - exact fderivWithin_inter h (uniqueDiffOn_univ _ (mem_univ _)) + simp only [fderiv, fderivWithin, HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.2 h] #align fderiv_within_of_mem_nhds fderivWithin_of_mem_nhds +@[simp] +theorem fderivWithin_univ : fderivWithin 𝕜 f univ = fderiv 𝕜 f := + funext fun _ => fderivWithin_of_mem_nhds univ_mem +#align fderiv_within_univ fderivWithin_univ + theorem fderivWithin_of_open (hs : IsOpen s) (hx : x ∈ s) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x := - fderivWithin_of_mem_nhds (IsOpen.mem_nhds hs hx) + fderivWithin_of_mem_nhds (hs.mem_nhds hx) #align fderiv_within_of_open fderivWithin_of_open theorem fderivWithin_eq_fderiv (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableAt 𝕜 f x) : @@ -798,7 +775,51 @@ end Continuous section congr /-! ### congr properties of the derivative -/ - +theorem hasFDerivWithinAt_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) : + HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x := + calc + HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' (s \ {y}) x := + (hasFDerivWithinAt_diff_singleton _).symm + _ ↔ HasFDerivWithinAt f f' (t \ {y}) x := by + suffices 𝓝[s \ {y}] x = 𝓝[t \ {y}] x by simp only [HasFDerivWithinAt, this] + simpa only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter', diff_eq, + inter_comm] using h + _ ↔ HasFDerivWithinAt f f' t x := hasFDerivWithinAt_diff_singleton _ +#align has_fderiv_within_at_congr_set' hasFDerivWithinAt_congr_set' + +theorem hasFDerivWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) : + HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x := + hasFDerivWithinAt_congr_set' x <| h.filter_mono inf_le_left +#align has_fderiv_within_at_congr_set hasFDerivWithinAt_congr_set + +theorem differentiableWithinAt_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) : + DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x := + exists_congr fun _ => hasFDerivWithinAt_congr_set' _ h +#align differentiable_within_at_congr_set' differentiableWithinAt_congr_set' + +theorem differentiableWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) : + DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x := + exists_congr fun _ => hasFDerivWithinAt_congr_set h +#align differentiable_within_at_congr_set differentiableWithinAt_congr_set + +theorem fderivWithin_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) : + fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x := by + simp only [fderivWithin, hasFDerivWithinAt_congr_set' y h] +#align fderiv_within_congr_set' fderivWithin_congr_set' + +theorem fderivWithin_congr_set (h : s =ᶠ[𝓝 x] t) : fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x := + fderivWithin_congr_set' x <| h.filter_mono inf_le_left +#align fderiv_within_congr_set fderivWithin_congr_set + +theorem fderivWithin_eventually_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) : + fderivWithin 𝕜 f s =ᶠ[𝓝 x] fderivWithin 𝕜 f t := + (eventually_nhds_nhdsWithin.2 h).mono fun _ => fderivWithin_congr_set' y +#align fderiv_within_eventually_congr_set' fderivWithin_eventually_congr_set' + +theorem fderivWithin_eventually_congr_set (h : s =ᶠ[𝓝 x] t) : + fderivWithin 𝕜 f s =ᶠ[𝓝 x] fderivWithin 𝕜 f t := + fderivWithin_eventually_congr_set' x <| h.filter_mono inf_le_left +#align fderiv_within_eventually_congr_set fderivWithin_eventually_congr_set theorem Filter.EventuallyEq.hasStrictFDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) (h' : ∀ y, f₀' y = f₁' y) : HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x := by @@ -853,19 +874,19 @@ theorem Filter.EventuallyEq.differentiableWithinAt_iff_of_mem (h : f₀ =ᶠ[ h.differentiableWithinAt_iff (h.eq_of_nhdsWithin hx) #align filter.eventually_eq.differentiable_within_at_iff_of_mem Filter.EventuallyEq.differentiableWithinAt_iff_of_mem -theorem HasFDerivWithinAt.congr_mono (h : HasFDerivWithinAt f f' s x) (ht : ∀ x ∈ t, f₁ x = f x) +theorem HasFDerivWithinAt.congr_mono (h : HasFDerivWithinAt f f' s x) (ht : EqOn f₁ f t) (hx : f₁ x = f x) (h₁ : t ⊆ s) : HasFDerivWithinAt f₁ f' t x := HasFDerivAtFilter.congr_of_eventuallyEq (h.mono h₁) (Filter.mem_inf_of_right ht) hx #align has_fderiv_within_at.congr_mono HasFDerivWithinAt.congr_mono -theorem HasFDerivWithinAt.congr (h : HasFDerivWithinAt f f' s x) (hs : ∀ x ∈ s, f₁ x = f x) +theorem HasFDerivWithinAt.congr (h : HasFDerivWithinAt f f' s x) (hs : EqOn f₁ f s) (hx : f₁ x = f x) : HasFDerivWithinAt f₁ f' s x := h.congr_mono hs hx (Subset.refl _) #align has_fderiv_within_at.congr HasFDerivWithinAt.congr -theorem HasFDerivWithinAt.congr' (h : HasFDerivWithinAt f f' s x) (hs : ∀ x ∈ s, f₁ x = f x) - (hx : x ∈ s) : HasFDerivWithinAt f₁ f' s x := - h.congr hs (hs x hx) +theorem HasFDerivWithinAt.congr' (h : HasFDerivWithinAt f f' s x) (hs : EqOn f₁ f s) (hx : x ∈ s) : + HasFDerivWithinAt f₁ f' s x := + h.congr hs (hs hx) #align has_fderiv_within_at.congr' HasFDerivWithinAt.congr' theorem HasFDerivWithinAt.congr_of_eventuallyEq (h : HasFDerivWithinAt f f' s x) @@ -878,8 +899,8 @@ theorem HasFDerivAt.congr_of_eventuallyEq (h : HasFDerivAt f f' x) (h₁ : f₁ HasFDerivAtFilter.congr_of_eventuallyEq h h₁ (mem_of_mem_nhds h₁ : _) #align has_fderiv_at.congr_of_eventually_eq HasFDerivAt.congr_of_eventuallyEq -theorem DifferentiableWithinAt.congr_mono (h : DifferentiableWithinAt 𝕜 f s x) - (ht : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) : DifferentiableWithinAt 𝕜 f₁ t x := +theorem DifferentiableWithinAt.congr_mono (h : DifferentiableWithinAt 𝕜 f s x) (ht : EqOn f₁ f t) + (hx : f₁ x = f x) (h₁ : t ⊆ s) : DifferentiableWithinAt 𝕜 f₁ t x := (HasFDerivWithinAt.congr_mono h.hasFDerivWithinAt ht hx h₁).differentiableWithinAt #align differentiable_within_at.congr_mono DifferentiableWithinAt.congr_mono @@ -913,44 +934,46 @@ theorem DifferentiableAt.congr_of_eventuallyEq (h : DifferentiableAt 𝕜 f x) ( #align differentiable_at.congr_of_eventually_eq DifferentiableAt.congr_of_eventuallyEq theorem DifferentiableWithinAt.fderivWithin_congr_mono (h : DifferentiableWithinAt 𝕜 f s x) - (hs : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) : + (hs : EqOn f₁ f t) (hx : f₁ x = f x) (hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) : fderivWithin 𝕜 f₁ t x = fderivWithin 𝕜 f s x := (HasFDerivWithinAt.congr_mono h.hasFDerivWithinAt hs hx h₁).fderivWithin hxt #align differentiable_within_at.fderiv_within_congr_mono DifferentiableWithinAt.fderivWithin_congr_mono -theorem Filter.EventuallyEq.fderivWithin_eq (hs : UniqueDiffWithinAt 𝕜 s x) (hL : f₁ =ᶠ[𝓝[s] x] f) - (hx : f₁ x = f x) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := - if h : DifferentiableWithinAt 𝕜 f s x then - HasFDerivWithinAt.fderivWithin (h.hasFDerivWithinAt.congr_of_eventuallyEq hL hx) hs - else by - have h' : ¬DifferentiableWithinAt 𝕜 f₁ s x := - mt (fun h => h.congr_of_eventuallyEq (hL.mono fun x => Eq.symm) hx.symm) h - rw [fderivWithin_zero_of_not_differentiableWithinAt h, - fderivWithin_zero_of_not_differentiableWithinAt h'] +theorem Filter.EventuallyEq.fderivWithin_eq (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : + fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := by + simp only [fderivWithin, hs.hasFDerivWithinAt_iff hx] #align filter.eventually_eq.fderiv_within_eq Filter.EventuallyEq.fderivWithin_eq -theorem Filter.EventuallyEq.fderivWithin_eq_nhds (hs : UniqueDiffWithinAt 𝕜 s x) - (hL : f₁ =ᶠ[𝓝 x] f) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := - (show f₁ =ᶠ[𝓝[s] x] f from nhdsWithin_le_nhds hL).fderivWithin_eq hs (mem_of_mem_nhds hL : _) +theorem Filter.EventuallyEq.fderiv_within' (hs : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) : + fderivWithin 𝕜 f₁ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 f t := + (eventually_nhdsWithin_nhdsWithin.2 hs).mp <| + eventually_mem_nhdsWithin.mono fun _y hys hs => + EventuallyEq.fderivWithin_eq (hs.filter_mono <| nhdsWithin_mono _ ht) + (hs.self_of_nhdsWithin hys) +#align filter.eventually_eq.fderiv_within' Filter.EventuallyEq.fderiv_within' + +protected theorem Filter.EventuallyEq.fderivWithin (hs : f₁ =ᶠ[𝓝[s] x] f) : + fderivWithin 𝕜 f₁ s =ᶠ[𝓝[s] x] fderivWithin 𝕜 f s := + hs.fderiv_within' Subset.rfl +#align filter.eventually_eq.fderiv_within Filter.EventuallyEq.fderivWithin + +theorem Filter.EventuallyEq.fderivWithin_eq_nhds (h : f₁ =ᶠ[𝓝 x] f) : + fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := + (h.filter_mono nhdsWithin_le_nhds).fderivWithin_eq h.self_of_nhds #align filter.eventually_eq.fderiv_within_eq_nhds Filter.EventuallyEq.fderivWithin_eq_nhds -theorem fderivWithin_congr (hs : UniqueDiffWithinAt 𝕜 s x) (hL : ∀ y ∈ s, f₁ y = f y) - (hx : f₁ x = f x) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := by - apply Filter.EventuallyEq.fderivWithin_eq hs _ hx - apply mem_of_superset self_mem_nhdsWithin - exact hL +theorem fderivWithin_congr (hs : EqOn f₁ f s) (hx : f₁ x = f x) : + fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := + (hs.eventuallyEq.filter_mono inf_le_right).fderivWithin_eq hx #align fderiv_within_congr fderivWithin_congr -theorem fderivWithin_congr' (hs : UniqueDiffWithinAt 𝕜 s x) (hL : ∀ y ∈ s, f₁ y = f y) - (hx : x ∈ s) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := - fderivWithin_congr hs hL (hL x hx) +theorem fderivWithin_congr' (hs : EqOn f₁ f s) (hx : x ∈ s) : + fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := + fderivWithin_congr hs (hs hx) #align fderiv_within_congr' fderivWithin_congr' -theorem Filter.EventuallyEq.fderiv_eq (hL : f₁ =ᶠ[𝓝 x] f) : fderiv 𝕜 f₁ x = fderiv 𝕜 f x := by - have A : f₁ x = f x := hL.eq_of_nhds - rw [← fderivWithin_univ, ← fderivWithin_univ] - rw [← nhdsWithin_univ] at hL - exact hL.fderivWithin_eq uniqueDiffWithinAt_univ A +theorem Filter.EventuallyEq.fderiv_eq (h : f₁ =ᶠ[𝓝 x] f) : fderiv 𝕜 f₁ x = fderiv 𝕜 f x := by + rw [← fderivWithin_univ, ← fderivWithin_univ, h.fderivWithin_eq_nhds] #align filter.eventually_eq.fderiv_eq Filter.EventuallyEq.fderiv_eq protected theorem Filter.EventuallyEq.fderiv (h : f₁ =ᶠ[𝓝 x] f) : fderiv 𝕜 f₁ =ᶠ[𝓝 x] fderiv 𝕜 f := @@ -1128,14 +1151,15 @@ open Function variable (𝕜 : Type _) {E F : Type _} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} -theorem support_fderiv_subset : support (fderiv 𝕜 f) ⊆ tsupport f := by - intro x - rw [← not_imp_not] - intro h2x - rw [not_mem_tsupport_iff_eventuallyEq] at h2x - exact nmem_support.mpr (h2x.fderiv_eq.trans <| fderiv_const_apply 0) +theorem support_fderiv_subset : support (fderiv 𝕜 f) ⊆ tsupport f := fun x ↦ by + rw [← not_imp_not, not_mem_tsupport_iff_eventuallyEq, nmem_support] + exact fun hx => hx.fderiv_eq.trans <| fderiv_const_apply 0 #align support_fderiv_subset support_fderiv_subset +theorem tsupport_fderiv_subset : tsupport (fderiv 𝕜 f) ⊆ tsupport f := + closure_minimal (support_fderiv_subset 𝕜) isClosed_closure +#align tsupport_fderiv_subset tsupport_fderiv_subset + protected theorem HasCompactSupport.fderiv (hf : HasCompactSupport f) : HasCompactSupport (fderiv 𝕜 f) := hf.mono' <| support_fderiv_subset 𝕜