feat(analysis/calculus/deriv): Prove equivalence of Fréchet derivative and the classical definition (#1834)

* feat(analysis/calculus/deriv): Prove equivalence of Fréchet derivative and the classical definition

* Fix a typo

* Move, change doc, add versions for `has_deriv_within_at` and `has_deriv_at`.

* Fix docstring, remove an unsed argument

Author: urkud

src/analysis/calculus/deriv.lean

@@ -171,6 +171,37 @@ theorem has_deriv_at_iff_tendsto : has_deriv_at f f' x ↔
   tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (𝓝 x) (𝓝 0) :=
 has_fderiv_at_filter_iff_tendsto
 
+/-- If the domain has dimension one, then Fréchet derivative is equivalent to the classical
+definition with a limit. In this version we have to take the limit along the subset `-{x}`,
+because for `y=x` the slope equals zero due to the convention `0⁻¹=0`. -/
+lemma has_deriv_at_filter_iff_tendsto_slope {x : 𝕜} {L : filter 𝕜} :
+  has_deriv_at_filter f f' x L ↔
+    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (L ⊓ principal (-{x})) (𝓝 f') :=
+begin
+  conv_lhs { simp only [has_deriv_at_filter_iff_tendsto, (normed_field.norm_inv _).symm,
+    (norm_smul _ _).symm, tendsto_zero_iff_norm_tendsto_zero.symm] },
+  conv_rhs { rw [← nhds_translation f', tendsto_comap_iff] },
+  refine (tendsto_inf_principal_nhds_iff_of_forall_eq $ by simp).symm.trans (tendsto_congr' _),
+  rw mem_inf_principal,
+  refine univ_mem_sets' (λ z hz, _),
+  have : z ≠ x, by simpa [function.comp] using hz,
+  simp only [mem_set_of_eq],
+  rw [smul_sub, ← mul_smul, inv_mul_cancel (sub_ne_zero.2 this), one_smul]
+end
+
+lemma has_deriv_within_at_iff_tendsto_slope {x : 𝕜} {s : set 𝕜} :
+  has_deriv_within_at f f' s x ↔
+    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x (s \ {x})) (𝓝 f') :=
+begin
+  simp only [has_deriv_within_at, nhds_within, diff_eq, lattice.inf_assoc.symm, inf_principal.symm],
+  exact has_deriv_at_filter_iff_tendsto_slope
+end
+
+lemma has_deriv_at_iff_tendsto_slope {x : 𝕜} :
+  has_deriv_at f f' x ↔
+    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x (-{x})) (𝓝 f') :=
+has_deriv_at_filter_iff_tendsto_slope
+
 theorem has_deriv_at_iff_is_o_nhds_zero : has_deriv_at f f' x ↔
   is_o (λh, f (x + h) - f x - h • f') (λh, h) (𝓝 0) :=
 has_fderiv_at_iff_is_o_nhds_zero

src/analysis/calculus/fderiv.lean

@@ -235,7 +235,7 @@ have h : ∀ x', ∥x' - x∥ = 0 → ∥f x' - f x - f' (x' - x)∥ = 0, from 
 begin
   unfold has_fderiv_at_filter,
   rw [←is_o_norm_left, ←is_o_norm_right, is_o_iff_tendsto h],
-  exact tendsto.congr'r (λ _, div_eq_inv_mul),
+  exact tendsto_congr (λ _, div_eq_inv_mul),
 end
 
 theorem has_fderiv_within_at_iff_tendsto : has_fderiv_within_at f f' s x ↔
@@ -1344,7 +1344,7 @@ theorem has_fderiv_at_filter_real_equiv {L : filter E} :
   tendsto (λ x' : E, ∥x' - x∥⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0) :=
 begin
   symmetry,
-  rw [tendsto_iff_norm_tendsto_zero], refine tendsto.congr'r (λ x', _),
+  rw [tendsto_iff_norm_tendsto_zero], refine tendsto_congr (λ x', _),
   have : ∥x' + -x∥⁻¹ ≥ 0, from inv_nonneg.mpr (norm_nonneg _),
   simp [norm_smul, real.norm_eq_abs, abs_of_nonneg this]
 end

src/order/filter/basic.lean

@@ -1183,17 +1183,21 @@ lemma tendsto_iff_comap {f : α → β} {l₁ : filter α} {l₂ : filter β} :
   tendsto f l₁ l₂ ↔ l₁ ≤ l₂.comap f :=
 map_le_iff_le_comap
 
+lemma tendsto_congr' {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
+  (hl : {x | f₁ x = f₂ x} ∈ l₁) :  tendsto f₁ l₁ l₂ ↔ tendsto f₂ l₁ l₂ :=
+by rw [tendsto, tendsto, map_cong hl]
+
 lemma tendsto.congr' {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
   (hl : {x | f₁ x = f₂ x} ∈ l₁) (h : tendsto f₁ l₁ l₂) : tendsto f₂ l₁ l₂ :=
-by rwa [tendsto, ←map_cong hl]
+(tendsto_congr' hl).1 h
 
-theorem tendsto.congr'r {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
+theorem tendsto_congr {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
   (h : ∀ x, f₁ x = f₂ x) : tendsto f₁ l₁ l₂ ↔ tendsto f₂ l₁ l₂ :=
-iff_of_eq (by congr'; exact funext h)
+tendsto_congr' (univ_mem_sets' h)
 
 theorem tendsto.congr {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
   (h : ∀ x, f₁ x = f₂ x) : tendsto f₁ l₁ l₂ → tendsto f₂ l₁ l₂ :=
-(tendsto.congr'r h).1
+(tendsto_congr h).1
 
 lemma tendsto_id' {x y : filter α} : x ≤ y → tendsto id x y :=
 by simp only [tendsto, map_id, forall_true_iff] {contextual := tt}

src/topology/basic.lean

@@ -569,6 +569,23 @@ lemma mem_closure_of_tendsto {f : β → α} {b : filter β} {a : α} {s : set 
 mem_of_closed_of_tendsto hb hf (is_closed_closure) $
   filter.mem_sets_of_superset h (preimage_mono subset_closure)
 
+/-- Suppose that `f` sends the complement to `s` to a single point `a`, and `l` is some filter.
+Then `f` tends to `a` along `l` restricted to `s` if and only it tends to `a` along `l`. -/
+lemma tendsto_inf_principal_nhds_iff_of_forall_eq {f : β → α} {l : filter β} {s : set β}
+  {a : α} (h : ∀ x ∉ s, f x = a) :
+  tendsto f (l ⊓ principal s) (𝓝 a) ↔ tendsto f l (𝓝 a) :=
+begin
+  rw [tendsto_iff_comap, tendsto_iff_comap],
+  replace h : principal (-s) ≤ comap f (𝓝 a),
+  { rintros U ⟨t, ht, htU⟩ x hx,
+    have : f x ∈ t, from (h x hx).symm ▸ mem_of_nhds ht,
+    exact htU this },
+  refine ⟨λ h', _, le_trans inf_le_left⟩,
+  have := sup_le h' h,
+  rw [sup_inf_right, sup_principal, union_compl_self, principal_univ,
+    inf_top_eq, sup_le_iff] at this,
+  exact this.1
+end
 
 section lim
 variables [inhabited α]