refactor(analysis/calculus/fderiv): prove has_fderiv_within_at.lim …

…for any filter (#1805)

* refactor(analysis/calculus/fderiv): prove `has_fderiv_within_at.lim` for any filter

Also prove two versions of "directional derivative agrees with
`has_fderiv_at`": `has_fderiv_at.lim` and `has_fderiv_at.lim_real`.

* Rename a lemma as suggested by @sgouezel

src/analysis/calculus/fderiv.lean

@@ -155,38 +155,38 @@ uniqueness of the derivative. -/
 `c n * d n` tends to `v`, then `c n * (f (x + d n) - f x)` tends to `f' v`. This lemma expresses
 this fact, for functions having a derivative within a set. Its specific formulation is useful for
 tangent cone related discussions. -/
-theorem has_fderiv_within_at.lim (h : has_fderiv_within_at f f' s x)
-  {c : ℕ → 𝕜} {d : ℕ → E} {v : E} (dtop : {n : ℕ | x + d n ∈ s} ∈ (at_top : filter ℕ))
-  (clim : tendsto (λ (n : ℕ), ∥c n∥) at_top at_top)
-  (cdlim : tendsto (λ (n : ℕ), c n • d n) at_top (𝓝 v)) :
-  tendsto (λn, c n • (f (x + d n) - f x)) at_top (𝓝 (f' v)) :=
+theorem has_fderiv_within_at.lim (h : has_fderiv_within_at f f' s x) {α : Type*} (l : filter α)
+  {c : α → 𝕜} {d : α → E} {v : E} (dtop : {n | x + d n ∈ s} ∈ l)
+  (clim : tendsto (λ n, ∥c n∥) l at_top)
+  (cdlim : tendsto (λ n, c n • d n) l (𝓝 v)) :
+  tendsto (λn, c n • (f (x + d n) - f x)) l (𝓝 (f' v)) :=
 begin
-  have at_top_is_finer : at_top ≤ comap (λ (n : ℕ), x + d n) (nhds_within x s),
+  have at_top_is_finer : l ≤ comap (λ n, x + d n) (nhds_within x s),
   { conv in (nhds_within x s) { rw ← add_zero x },
     rw [← tendsto_iff_comap, nhds_within, tendsto_inf],
     split,
-    { apply tendsto_const_nhds.add (tangent_cone_at.lim_zero clim cdlim) },
+    { apply tendsto_const_nhds.add (tangent_cone_at.lim_zero l clim cdlim) },
     { rwa tendsto_principal } },
   have : is_o (λ y, f y - f x - f' (y - x)) (λ y, y - x) (nhds_within x s) := h,
-  have : is_o (λ n:ℕ, f (x + d n) - f x - f' ((x + d n) - x)) (λ n, (x + d n)  - x)
+  have : is_o (λ n, f (x + d n) - f x - f' ((x + d n) - x)) (λ n, (x + d n)  - x)
     ((nhds_within x s).comap (λn, x+ d n)) := is_o.comp this _,
-  have : is_o (λ n:ℕ, f (x + d n) - f x - f' (d n)) d
+  have : is_o (λ n, f (x + d n) - f x - f' (d n)) d
     ((nhds_within x s).comap (λn, x + d n)) := by simpa,
-  have : is_o (λn:ℕ, f (x + d n) - f x - f' (d n)) d at_top :=
+  have : is_o (λn, f (x + d n) - f x - f' (d n)) d l :=
     is_o.mono at_top_is_finer this,
-  have : is_o (λn:ℕ, c n • (f (x + d n) - f x - f' (d n))) (λn, c n • d n) at_top :=
+  have : is_o (λn, c n • (f (x + d n) - f x - f' (d n))) (λn, c n • d n) l :=
     is_o_smul this,
-  have : is_o (λn:ℕ, c n • (f (x + d n) - f x - f' (d n))) (λn, (1:ℝ)) at_top :=
+  have : is_o (λn, c n • (f (x + d n) - f x - f' (d n))) (λn, (1:ℝ)) l :=
     this.trans_is_O (is_O_one_of_tendsto cdlim),
-  have L1 : tendsto (λn:ℕ, c n • (f (x + d n) - f x - f' (d n))) at_top (𝓝 0) :=
+  have L1 : tendsto (λn, c n • (f (x + d n) - f x - f' (d n))) l (𝓝 0) :=
     is_o_one_iff.1 this,
-  have L2 : tendsto (λn:ℕ, f' (c n • d n)) at_top (𝓝 (f' v)) :=
+  have L2 : tendsto (λn, f' (c n • d n)) l (𝓝 (f' v)) :=
     tendsto.comp f'.cont.continuous_at cdlim,
-  have L3 : tendsto (λn:ℕ, (c n • (f (x + d n) - f x - f' (d n)) +  f' (c n • d n)))
-            at_top (𝓝 (0 + f' v)) :=
+  have L3 : tendsto (λn, (c n • (f (x + d n) - f x - f' (d n)) +  f' (c n • d n)))
+            l (𝓝 (0 + f' v)) :=
     L1.add L2,
-  have : (λn:ℕ, (c n • (f (x + d n) - f x - f' (d n)) +  f' (c n • d n)))
-          = (λn: ℕ, c n • (f (x + d n) - f x)),
+  have : (λn, (c n • (f (x + d n) - f x - f' (d n)) +  f' (c n • d n)))
+          = (λn, c n • (f (x + d n) - f x)),
     by { ext n, simp [smul_add] },
   rwa [this, zero_add] at L3
 end
@@ -197,7 +197,7 @@ theorem unique_diff_within_at.eq (H : unique_diff_within_at 𝕜 s x)
 begin
   have A : ∀y ∈ tangent_cone_at 𝕜 s x, f' y = f₁' y,
   { rintros y ⟨c, d, dtop, clim, cdlim⟩,
-    exact tendsto_nhds_unique (by simp) (h.lim dtop clim cdlim) (h₁.lim dtop clim cdlim) },
+    exact tendsto_nhds_unique (by simp) (h.lim at_top dtop clim cdlim) (h₁.lim at_top dtop clim cdlim) },
   have B : ∀y ∈ submodule.span 𝕜 (tangent_cone_at 𝕜 s x), f' y = f₁' y,
   { assume y hy,
     apply submodule.span_induction hy,
@@ -291,6 +291,20 @@ lemma has_fderiv_at.differentiable_at (h : has_fderiv_at f f' x) : differentiabl
   has_fderiv_within_at f f' univ x ↔ has_fderiv_at f f' x :=
 by { simp only [has_fderiv_within_at, nhds_within_univ], refl }
 
+/-- Directional derivative agrees with `has_fderiv`. -/
+lemma has_fderiv_at.lim (hf : has_fderiv_at f f' x) (v : E) {α : Type*} {c : α → 𝕜}
+  {l : filter α} (hc : tendsto (λ n, ∥c n∥) l at_top) :
+  tendsto (λ n, (c n) • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 (f' v)) :=
+begin
+  refine (has_fderiv_within_at_univ.2 hf).lim _ (univ_mem_sets' (λ _, trivial)) hc _,
+  assume U hU,
+  apply mem_sets_of_superset (ne_mem_of_tendsto_norm_at_top hc (0:𝕜)) _,
+  assume y hy,
+  rw [mem_preimage],
+  convert mem_of_nhds hU,
+  rw [← mul_smul, mul_inv_cancel hy, one_smul]
+end
+
 theorem has_fderiv_at_unique
   (h₀ : has_fderiv_at f f₀' x) (h₁ : has_fderiv_at f f₁' x) : f₀' = f₁' :=
 begin
@@ -1314,9 +1328,9 @@ section
 
 variables {E : Type*} [normed_group E] [normed_space ℝ E]
 variables {F : Type*} [normed_group F] [normed_space ℝ F]
-variables {G : Type*} [normed_group G] [normed_space ℝ G]
+variables {f : E → F} {f' : E →L[ℝ] F} {x : E}
 
-theorem has_fderiv_at_filter_real_equiv {f : E → F} {f' : E →L[ℝ] F} {x : E} {L : filter E} :
+theorem has_fderiv_at_filter_real_equiv {L : filter E} :
   tendsto (λ x' : E, ∥x' - x∥⁻¹ * ∥f x' - f x - f' (x' - x)∥) L (𝓝 0) ↔
   tendsto (λ x' : E, ∥x' - x∥⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0) :=
 begin
@@ -1326,6 +1340,14 @@ begin
   simp [norm_smul, real.norm_eq_abs, abs_of_nonneg this]
 end
 
+lemma has_fderiv_at.lim_real (hf : has_fderiv_at f f' x) (v : E) :
+  tendsto (λ (c:ℝ), c • (f (x + c⁻¹ • v) - f x)) at_top (𝓝 (f' v)) :=
+begin
+  apply hf.lim v,
+  rw tendsto_at_top_at_top,
+  exact λ b, ⟨b, λ a ha, le_trans ha (le_abs_self _)⟩
+end
+
 end
 
 section tangent_cone
@@ -1342,7 +1364,7 @@ lemma has_fderiv_within_at.image_tangent_cone_subset {x : E} (h : has_fderiv_wit
 begin
   rw image_subset_iff,
   rintros v ⟨c, d, dtop, clim, cdlim⟩,
-  refine ⟨c, (λn, f (x + d n) - f x), mem_sets_of_superset dtop _, clim, h.lim dtop clim cdlim⟩,
+  refine ⟨c, (λn, f (x + d n) - f x), mem_sets_of_superset dtop _, clim, h.lim at_top dtop clim cdlim⟩,
   simp [-mem_image, mem_image_of_mem] {contextual := tt}
 end
 

src/analysis/calculus/tangent_cone.lean

@@ -91,24 +91,21 @@ end
 
 /-- Auxiliary lemma ensuring that, under the assumptions defining the tangent cone,
 the sequence `d` tends to 0 at infinity. -/
-lemma tangent_cone_at.lim_zero {c : ℕ → 𝕜} {d : ℕ → E}
-  (hc : tendsto (λn, ∥c n∥) at_top at_top) (hd : tendsto (λn, c n • d n) at_top (𝓝 y)) :
-  tendsto d at_top (𝓝 0) :=
+lemma tangent_cone_at.lim_zero {α : Type*} (l : filter α) {c : α → 𝕜} {d : α → E}
+  (hc : tendsto (λn, ∥c n∥) l at_top) (hd : tendsto (λn, c n • d n) l (𝓝 y)) :
+  tendsto d l (𝓝 0) :=
 begin
-  have A : tendsto (λn, ∥c n∥⁻¹) at_top (𝓝 0) :=
+  have A : tendsto (λn, ∥c n∥⁻¹) l (𝓝 0) :=
     tendsto_inverse_at_top_nhds_0.comp hc,
-  have B : tendsto (λn, ∥c n • d n∥) at_top (𝓝 ∥y∥) :=
+  have B : tendsto (λn, ∥c n • d n∥) l (𝓝 ∥y∥) :=
     (continuous_norm.tendsto _).comp hd,
-  have C : tendsto (λn, ∥c n∥⁻¹ * ∥c n • d n∥) at_top (𝓝 (0 * ∥y∥)) := A.mul B,
+  have C : tendsto (λn, ∥c n∥⁻¹ * ∥c n • d n∥) l (𝓝 (0 * ∥y∥)) := A.mul B,
   rw zero_mul at C,
-  have : {n | ∥c n∥⁻¹ * ∥c n • d n∥ = ∥d n∥} ∈ (@at_top ℕ _),
-  { have : {n | 1 ≤ ∥c n∥} ∈ (@at_top ℕ _) :=
-      hc (mem_at_top 1),
-    apply mem_sets_of_superset this (λn hn, _),
-    rw mem_set_of_eq at hn,
-    rw [mem_set_of_eq, ← norm_inv, ← norm_smul, smul_smul, inv_mul_cancel, one_smul],
-    simpa [norm_eq_zero] using (ne_of_lt (lt_of_lt_of_le zero_lt_one hn)).symm },
-  have D : tendsto (λ (n : ℕ), ∥d n∥) at_top (𝓝 0) :=
+  have : {n | ∥c n∥⁻¹ * ∥c n • d n∥ = ∥d n∥} ∈ l,
+  { apply mem_sets_of_superset (ne_mem_of_tendsto_norm_at_top hc 0) (λn hn, _),
+    rw [mem_set_of_eq, norm_smul, ← mul_assoc, inv_mul_cancel, one_mul],
+    rwa [ne.def, norm_eq_zero] },
+  have D : tendsto (λ n, ∥d n∥) l (𝓝 0) :=
     tendsto.congr' this C,
   rw tendsto_zero_iff_norm_tendsto_zero,
   exact D
@@ -123,7 +120,7 @@ begin
   refine ⟨c, d, _, ctop, clim⟩,
   have : {n : ℕ | x + d n ∈ t} ∈ at_top,
   { have : tendsto (λn, x + d n) at_top (𝓝 (x + 0)) :=
-      tendsto_const_nhds.add (tangent_cone_at.lim_zero ctop clim),
+      tendsto_const_nhds.add (tangent_cone_at.lim_zero at_top ctop clim),
     rw add_zero at this,
     exact mem_map.1 (this ht) },
   exact inter_mem_sets ds this

src/analysis/normed_space/basic.lean

@@ -276,6 +276,19 @@ end
 lemma continuous_nnnorm : continuous (nnnorm : α → nnreal) :=
 continuous_subtype_mk _ continuous_norm
 
+/-- If `∥y∥→∞`, then we can assume `y≠x` for any fixed `x`. -/
+lemma ne_mem_of_tendsto_norm_at_top {l : filter γ} {f : γ → α}
+  (h : tendsto (λ y, ∥f y∥) l at_top) (x : α) :
+  {y | f y ≠ x} ∈ l :=
+begin
+  have : {y | 1 + ∥x∥ ≤ ∥f y∥} ∈ l := h (mem_at_top (1 + ∥x∥)),
+  apply mem_sets_of_superset this,
+  assume y hy hxy,
+  subst x,
+  simp at hy,
+  exact not_le_of_lt zero_lt_one hy
+end
+
 /-- A normed group is a uniform additive group, i.e., addition and subtraction are uniformly
 continuous. -/
 @[priority 100] -- see Note [lower instance priority]