feat(Analysis/Calculus/Deriv/Inverse): add deriv_zero_of_frequently_mem (leanprover-community#34576)

This PR proves that if a function frequently (in `𝓝[s ∖ {x}]`) takes values in a set `t` that does not
accumulate at `f x`, then its derivative at `x` equals zero. The application that I have in mind is where this set is closed and discrete (and thus has no accumulation points).

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Analysis/Calculus/Deriv/Inverse.lean

@@ -89,19 +89,32 @@ theorem OpenPartialHomeomorph.hasDerivAt_symm (f : OpenPartialHomeomorph 𝕜 
     HasDerivAt f.symm f'⁻¹ a :=
   htff'.of_local_left_inverse (f.symm.continuousAt ha) hf' (f.eventually_right_inverse ha)
 
+theorem HasDerivWithinAt.tendsto_nhdsWithin_nhdsNE (h : HasDerivWithinAt f f' s x) (hf' : f' ≠ 0) :
+    Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x) :=
+  h.hasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE ⟨‖f'‖₊⁻¹, AntilipschitzWith.of_le_mul_dist
+    fun _ _ ↦ by simp [dist_eq_norm_sub, ← sub_smul, norm_smul]; field_simp; rfl⟩
+
 theorem HasDerivWithinAt.eventually_ne (h : HasDerivWithinAt f f' s x) (hf' : f' ≠ 0) :
     ∀ᶠ z in 𝓝[s \ {x}] x, f z ≠ c :=
-  h.hasFDerivWithinAt.eventually_ne
-    ⟨‖f'‖⁻¹, fun z => by simp [norm_smul]; field_simp; rfl⟩
+  h.hasFDerivWithinAt.eventually_ne ⟨‖f'‖₊⁻¹, AntilipschitzWith.of_le_mul_dist
+    fun _ _ ↦ by simp [dist_eq_norm_sub, ← sub_smul, norm_smul]; field_simp; rfl⟩
+
+theorem HasDerivWithinAt.eventually_notMem (h : HasDerivWithinAt f f' s x) (hf' : f' ≠ 0)
+    (t : Set F) (ht : ¬ AccPt (f x) (𝓟 t)) : ∀ᶠ z in 𝓝[s \ {x}] x, f z ∉ t :=
+  h.hasFDerivWithinAt.eventually_notMem ⟨‖f'‖₊⁻¹, AntilipschitzWith.of_le_mul_dist
+    fun _ _ ↦ by simp [dist_eq_norm_sub, ← sub_smul, norm_smul]; field_simp; rfl⟩ t ht
+
+theorem HasDerivAt.tendsto_nhdsNE (h : HasDerivAt f f' x) (hf' : f' ≠ 0) :
+    Tendsto f (𝓝[≠] x) (𝓝[≠] f x) := by
+  simpa only [compl_eq_univ_diff] using (hasDerivWithinAt_univ.2 h).tendsto_nhdsWithin_nhdsNE hf'
 
 theorem HasDerivAt.eventually_ne (h : HasDerivAt f f' x) (hf' : f' ≠ 0) :
     ∀ᶠ z in 𝓝[≠] x, f z ≠ c := by
   simpa only [compl_eq_univ_diff] using (hasDerivWithinAt_univ.2 h).eventually_ne hf'
 
-theorem HasDerivAt.tendsto_nhdsNE (h : HasDerivAt f f' x) (hf' : f' ≠ 0) :
-    Tendsto f (𝓝[≠] x) (𝓝[≠] f x) :=
-  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ h.continuousAt.continuousWithinAt
-    (h.eventually_ne hf')
+theorem HasDerivAt.eventually_notMem (h : HasDerivAt f f' x) (hf' : f' ≠ 0)
+    (t : Set F) (ht : ¬ AccPt (f x) (𝓟 t)) : ∀ᶠ z in 𝓝[≠] x, f z ∉ t := by
+  simpa only [compl_eq_univ_diff] using (hasDerivWithinAt_univ.2 h).eventually_notMem hf' t ht
 
 /-- If a function is equal to a constant at a set of points that accumulates to `x` in `s`,
 then its derivative within `s` at `x` equals zero,
@@ -113,13 +126,31 @@ theorem derivWithin_zero_of_frequently_const {c} (h : ∃ᶠ y in 𝓝[s \ {x}]
     exact hf.hasDerivWithinAt.eventually_ne h
   · exact derivWithin_zero_of_not_differentiableWithinAt hf
 
+/-- If a function frequently (in `𝓝[s ∖ {x}] x`) takes values in a set `t` that does not
+accumulate at `f x`, then its derivative within `s` at `x` equals zero,
+either because it has derivative zero or because it isn't differentiable at this point. -/
+theorem derivWithin_zero_of_frequently_mem (t : Set F) (ht : ¬ AccPt (f x) (𝓟 t))
+    (h : ∃ᶠ y in 𝓝[s \ {x}] x, f y ∈ t) : derivWithin f s x = 0 := by
+  by_cases hf : DifferentiableWithinAt 𝕜 f s x
+  · contrapose! h
+    exact hf.hasDerivWithinAt.eventually_notMem h t ht
+  · exact derivWithin_zero_of_not_differentiableWithinAt hf
+
 /-- If a function is equal to a constant at a set of points that accumulates to `x`,
 then its derivative at `x` equals zero,
 either because it has derivative zero or because it isn't differentiable at this point. -/
 theorem deriv_zero_of_frequently_const {c} (h : ∃ᶠ y in 𝓝[≠] x, f y = c) : deriv f x = 0 := by
   rw [← derivWithin_univ, derivWithin_zero_of_frequently_const]
   rwa [← compl_eq_univ_diff]
 
+/-- If a function frequently (in `𝓝[≠] x`) takes values in a set `t` that does not
+accumulate at `f x`, then its derivative at `x` equals zero,
+either because it has derivative zero or because it isn't differentiable at this point. -/
+theorem deriv_zero_of_frequently_mem (t : Set F) (ht : ¬ AccPt (f x) (𝓟 t))
+    (h : ∃ᶠ y in 𝓝[≠] x, f y ∈ t) : deriv f x = 0 := by
+  rw [← derivWithin_univ, derivWithin_zero_of_frequently_mem t ht]
+  rwa [← compl_eq_univ_diff]
+
 theorem not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero {f g : 𝕜 → 𝕜} {a : 𝕜}
     {s t : Set 𝕜} (ha : a ∈ s) (hsu : UniqueDiffWithinAt 𝕜 s a) (hf : HasDerivWithinAt f 0 t (g a))
     (hst : MapsTo g s t) (hfg : f ∘ g =ᶠ[𝓝[s] a] id) : ¬DifferentiableWithinAt 𝕜 g s a := by

Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

@@ -404,20 +404,46 @@ theorem OpenPartialHomeomorph.hasFDerivAt_symm (f : OpenPartialHomeomorph E F) {
     HasFDerivAt f.symm (f'.symm : F →L[𝕜] E) a :=
   htff'.of_local_left_inverse (f.symm.continuousAt ha) (f.eventually_right_inverse ha)
 
+theorem HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE (h : HasFDerivWithinAt f f' s x)
+    (hf' : ∃ C, AntilipschitzWith C f') : Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x) := by
+  replace hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖ := by
+    obtain ⟨C, hC⟩ := hf'
+    exact ⟨C, fun x ↦ by simpa using hC.le_mul_dist 0 x⟩
+  have A : (fun z ↦ z - x) =O[𝓝[s] x] fun z ↦ f' (z - x) :=
+    isBigO_iff.mpr <| hf'.imp fun C hC ↦ Eventually.of_forall fun z ↦ hC (z - x)
+  have : (fun z ↦ f z - f x) ~[𝓝[s] x] fun z ↦ f' (z - x) := h.isLittleO.trans_isBigO A
+  have : ∀ᶠ (x_1 : E) in 𝓝[s] x, x_1 ∈ ({x}ᶜ : Set E) → f x_1 ∈ ({f x}ᶜ : Set F) := by
+    simpa [sub_eq_zero, not_imp_not] using (A.trans this.isBigO_symm).eq_zero_imp
+  apply le_inf ((map_mono (nhdsWithin_mono x diff_subset)).trans h.continuousWithinAt)
+  rwa [le_principal_iff, ← eventually_mem_set, eventually_map, diff_eq, nhdsWithin_inter',
+    eventually_inf_principal]
+
 theorem HasFDerivWithinAt.eventually_ne (h : HasFDerivWithinAt f f' s x)
-    (hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖) : ∀ᶠ z in 𝓝[s \ {x}] x, f z ≠ c := by
+    (hf' : ∃ C, AntilipschitzWith C f') : ∀ᶠ z in 𝓝[s \ {x}] x, f z ≠ c := by
+  rw [← eventually_map (m := f) (P := fun z ↦ z ≠ c)]
+  apply Eventually.filter_mono (h.tendsto_nhdsWithin_nhdsNE hf')
   rcases eq_or_ne (f x) c with rfl | hc
-  · rw [nhdsWithin, diff_eq, ← inf_principal, ← inf_assoc, eventually_inf_principal]
-    have A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x) :=
-      isBigO_iff.2 <| hf'.imp fun C hC => Eventually.of_forall fun z => hC _
-    have : (fun z => f z - f x) ~[𝓝[s] x] fun z => f' (z - x) := h.isLittleO.trans_isBigO A
-    simpa [not_imp_not, sub_eq_zero] using (A.trans this.isBigO_symm).eq_zero_imp
-  · exact (h.continuousWithinAt.eventually_ne hc).filter_mono <| by gcongr; apply diff_subset
-
-theorem HasFDerivAt.eventually_ne (h : HasFDerivAt f f' x) (hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖) :
+  · exact eventually_mem_nhdsWithin
+  · exact eventually_ne_nhdsWithin hc
+
+theorem HasFDerivWithinAt.eventually_notMem (h : HasFDerivWithinAt f f' s x)
+    (hf' : ∃ C, AntilipschitzWith C f') (t : Set F) (ht : ¬ AccPt (f x) (𝓟 t)) :
+    ∀ᶠ z in 𝓝[s \ {x}] x, f z ∉ t := by
+  rw [accPt_iff_frequently_nhdsNE, not_frequently] at ht
+  exact eventually_map.mp (ht.filter_mono (h.tendsto_nhdsWithin_nhdsNE hf'))
+
+theorem HasFDerivAt.tendsto_nhdsNE (h : HasFDerivAt f f' x)
+    (hf' : ∃ C, AntilipschitzWith C f') : Tendsto f (𝓝[≠] x) (𝓝[≠] f x) := by
+  simpa only [compl_eq_univ_diff] using (hasFDerivWithinAt_univ.2 h).tendsto_nhdsWithin_nhdsNE hf'
+
+theorem HasFDerivAt.eventually_ne (h : HasFDerivAt f f' x) (hf' : ∃ C, AntilipschitzWith C f') :
     ∀ᶠ z in 𝓝[≠] x, f z ≠ c := by
   simpa only [compl_eq_univ_diff] using (hasFDerivWithinAt_univ.2 h).eventually_ne hf'
 
+theorem HasFDerivAt.eventually_notMem (h : HasFDerivAt f f' x) (hf' : ∃ C, AntilipschitzWith C f')
+    (t : Set F) (ht : ¬ AccPt (f x) (𝓟 t)) : ∀ᶠ z in 𝓝[≠] x, f z ∉ t := by
+  simpa only [compl_eq_univ_diff] using (hasFDerivWithinAt_univ.2 h).eventually_notMem hf' t ht
+
 end
 
 section