chore(analysis/calculus/{fderiv,deriv}): f x ≠ f a for x ≈ a, `x …

…≠ a` if `∥z∥ ≤ C * ∥f' z∥` (#5420)

src/analysis/asymptotics.lean

@@ -535,6 +535,12 @@ is_O_snd_prod.trans_is_o h
   is_o (λ x, (f' x, g' x)) k' l ↔ is_o f' k' l ∧ is_o g' k' l :=
 ⟨λ h, ⟨h.prod_left_fst, h.prod_left_snd⟩, λ h, h.1.prod_left h.2⟩
 
+lemma is_O_with.eq_zero_imp (h : is_O_with c f' g' l) : ∀ᶠ x in l, g' x = 0 → f' x = 0 :=
+eventually.mono h $ λ x hx hg, norm_le_zero_iff.1 $ by simpa [hg] using hx
+
+lemma is_O.eq_zero_imp (h : is_O f' g' l) : ∀ᶠ x in l, g' x = 0 → f' x = 0 :=
+let ⟨C, hC⟩ := h in hC.eq_zero_imp
+
 /-! ### Addition and subtraction -/
 
 section add_sub

src/analysis/calculus/deriv.lean

@@ -1460,6 +1460,11 @@ lemma local_homeomorph.has_deriv_at_symm (f : local_homeomorph 𝕜 𝕜) {a f'
   has_deriv_at f.symm f'⁻¹ a :=
 htff'.of_local_left_inverse (f.symm.continuous_at ha) hf' (f.eventually_right_inverse ha)
 
+lemma has_deriv_at.eventually_ne (h : has_deriv_at f f' x) (hf' : f' ≠ 0) :
+  ∀ᶠ z in 𝓝[{x}ᶜ] x, f z ≠ f x :=
+(has_deriv_at_iff_has_fderiv_at.1 h).eventually_ne
+  ⟨∥f'∥⁻¹, λ z, by field_simp [norm_smul, mt norm_eq_zero.1 hf']⟩
+
 theorem not_differentiable_within_at_of_local_left_inverse_has_deriv_within_at_zero
   {f g : 𝕜 → 𝕜} {a : 𝕜} {s t : set 𝕜} (ha : a ∈ s) (hsu : unique_diff_within_at 𝕜 s a)
   (hf : has_deriv_within_at f 0 t (g a)) (hst : maps_to g s t) (hfg : f ∘ g =ᶠ[𝓝[s] a] id) :

src/analysis/calculus/fderiv.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Sébastien Gouëzel, Yury Kudryashov
 -/
 import analysis.calculus.tangent_cone
 import analysis.normed_space.units
+import analysis.asymptotic_equivalent
 
 /-!
 # The Fréchet derivative
@@ -112,7 +113,7 @@ derivative, differentiable, Fréchet, calculus
 -/
 
 open filter asymptotics continuous_linear_map set metric
-open_locale topological_space classical nnreal
+open_locale topological_space classical nnreal asymptotics filter
 
 noncomputable theory
 
@@ -2470,6 +2471,21 @@ lemma local_homeomorph.has_fderiv_at_symm (f : local_homeomorph E F) {f' : E ≃
   has_fderiv_at f.symm (f'.symm : F →L[𝕜] E) a :=
 htff'.of_local_left_inverse (f.symm.continuous_at ha) (f.eventually_right_inverse ha)
 
+lemma has_fderiv_within_at.eventually_ne (h : has_fderiv_within_at f f' s x)
+  (hf' : ∃ C, ∀ z, ∥z∥ ≤ C * ∥f' z∥) :
+  ∀ᶠ z in 𝓝[s \ {x}] x, f z ≠ f x :=
+begin
+  rw [nhds_within, diff_eq, ← inf_principal, ← inf_assoc, eventually_inf_principal],
+  have A : is_O (λ z, z - x) (λ z, f' (z - x)) (𝓝[s] x) :=
+    (is_O_iff.2 $ hf'.imp $ λ C hC, eventually_of_forall $ λ z, hC _),
+  have : (λ z, f z - f x) ~[𝓝[s] x] (λ z, f' (z - x)) := h.trans_is_O A,
+  simpa [not_imp_not, sub_eq_zero] using (A.trans this.is_O_symm).eq_zero_imp
+end
+
+lemma has_fderiv_at.eventually_ne (h : has_fderiv_at f f' x) (hf' : ∃ C, ∀ z, ∥z∥ ≤ C * ∥f' z∥) :
+  ∀ᶠ z in 𝓝[{x}ᶜ] x, f z ≠ f x :=
+by simpa only [compl_eq_univ_diff] using (has_fderiv_within_at_univ.2 h).eventually_ne hf'
+
 end
 
 section

src/analysis/normed_space/operator_norm.lean

@@ -46,6 +46,10 @@ theorem linear_map.antilipschitz_of_bound {K : ℝ≥0} (h : ∀ x, ∥x∥ ≤
 antilipschitz_with.of_le_mul_dist $
 λ x y, by simpa only [dist_eq_norm, f.map_sub] using h (x - y)
 
+lemma linear_map.bound_of_antilipschitz {K : ℝ≥0} (h : antilipschitz_with K f) (x) :
+  ∥x∥ ≤ K * ∥f x∥ :=
+by simpa only [dist_zero_right, f.map_zero] using h.le_mul_dist x 0
+
 lemma linear_map.uniform_continuous_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   uniform_continuous f :=
 (f.lipschitz_of_bound C h).uniform_continuous

src/topology/local_homeomorph.lean

@@ -135,6 +135,11 @@ lemma eventually_right_inverse' (e : local_homeomorph α β) {x} (hx : x ∈ e.s
   ∀ᶠ y in 𝓝 (e x), e (e.symm y) = y :=
 e.eventually_right_inverse (e.map_source hx)
 
+lemma eventually_ne_nhds_within (e : local_homeomorph α β) {x} (hx : x ∈ e.source) :
+  ∀ᶠ x' in 𝓝[{x}ᶜ] x, e x' ≠ e x :=
+eventually_nhds_within_iff.2 $ (e.eventually_left_inverse hx).mono $
+  λ x' hx', mt $ λ h, by rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']
+
 lemma image_eq_target_inter_inv_preimage {s : set α} (h : s ⊆ e.source) :
   e '' s = e.target ∩ e.symm ⁻¹' s :=
 e.to_local_equiv.image_eq_target_inter_inv_preimage h