feat: port Analysis.Calculus.Deriv.Slope (#4444)

Mathlib.lean

@@ -421,6 +421,7 @@ import Mathlib.Analysis.Calculus.Deriv.Comp
 import Mathlib.Analysis.Calculus.Deriv.Linear
 import Mathlib.Analysis.Calculus.Deriv.Mul
 import Mathlib.Analysis.Calculus.Deriv.Prod
+import Mathlib.Analysis.Calculus.Deriv.Slope
 import Mathlib.Analysis.Calculus.FDeriv.Add
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Bilinear

Mathlib/Analysis/Calculus/Deriv/Slope.lean

@@ -0,0 +1,184 @@
+/-
+Copyright (c) 2019 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+
+! This file was ported from Lean 3 source module analysis.calculus.deriv.slope
+! leanprover-community/mathlib commit 3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.Calculus.Deriv.Basic
+import Mathlib.LinearAlgebra.AffineSpace.Slope
+
+/-!
+# Derivative as the limit of the slope
+
+In this file we relate the derivative of a function with its definition from a standard
+undergraduate course as the limit of the slope `(f y - f x) / (y - x)` as `y` tends to `𝓝[≠] x`.
+Since we are talking about functions taking values in a normed space instead of the base field, we
+use `slope f x y = (y - x)⁻¹ • (f y - f x)` instead of division.
+
+We also prove some estimates on the upper/lower limits of the slope in terms of the derivative.
+
+For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of
+`analysis/calculus/deriv/basic`.
+
+## Keywords
+
+derivative, slope
+-/
+
+
+universe u v w
+
+noncomputable section
+
+open Topology Filter
+open Filter Set
+
+section NormedField
+
+variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
+
+variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+
+variable {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+variable {f f₀ f₁ g : 𝕜 → F}
+
+variable {f' f₀' f₁' g' : F}
+
+variable {x : 𝕜}
+
+variable {s t : Set 𝕜}
+
+variable {L L₁ L₂ : Filter 𝕜}
+
+/-- 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`. -/
+theorem hasDerivAtFilter_iff_tendsto_slope {x : 𝕜} {L : Filter 𝕜} :
+    HasDerivAtFilter f f' x L ↔ Tendsto (slope f x) (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 f') :=
+  calc HasDerivAtFilter f f' x L
+    ↔ Tendsto (fun y ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') L (𝓝 0) := by
+        simp only [hasDerivAtFilter_iff_tendsto, ← norm_inv, ← norm_smul,
+          ← tendsto_zero_iff_norm_tendsto_zero, slope_def_module, smul_sub]
+  _ ↔ Tendsto (fun y ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 0) :=
+        .symm <| tendsto_inf_principal_nhds_iff_of_forall_eq <| by simp
+  _ ↔ Tendsto (fun y ↦ slope f x y - f') (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 0) := tendsto_congr' <| by
+        refine (EqOn.eventuallyEq fun y hy ↦ ?_).filter_mono inf_le_right
+        rw [inv_smul_smul₀ (sub_ne_zero.2 hy) f']
+  _ ↔ Tendsto (slope f x) (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 f') :=
+        by rw [← nhds_translation_sub f', tendsto_comap_iff]; rfl
+#align has_deriv_at_filter_iff_tendsto_slope hasDerivAtFilter_iff_tendsto_slope
+
+theorem hasDerivWithinAt_iff_tendsto_slope :
+    HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f') := by
+  simp only [HasDerivWithinAt, nhdsWithin, diff_eq, inf_assoc.symm, inf_principal.symm]
+  exact hasDerivAtFilter_iff_tendsto_slope
+#align has_deriv_within_at_iff_tendsto_slope hasDerivWithinAt_iff_tendsto_slope
+
+theorem hasDerivWithinAt_iff_tendsto_slope' (hs : x ∉ s) :
+    HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f') := by
+  rw [hasDerivWithinAt_iff_tendsto_slope, diff_singleton_eq_self hs]
+#align has_deriv_within_at_iff_tendsto_slope' hasDerivWithinAt_iff_tendsto_slope'
+
+theorem hasDerivAt_iff_tendsto_slope : HasDerivAt f f' x ↔ Tendsto (slope f x) (𝓝[≠] x) (𝓝 f') :=
+  hasDerivAtFilter_iff_tendsto_slope
+#align has_deriv_at_iff_tendsto_slope hasDerivAt_iff_tendsto_slope
+
+end NormedField
+
+/-! ### Upper estimates on liminf and limsup -/
+
+section Real
+
+variable {f : ℝ → ℝ} {f' : ℝ} {s : Set ℝ} {x : ℝ} {r : ℝ}
+
+theorem HasDerivWithinAt.limsup_slope_le (hf : HasDerivWithinAt f f' s x) (hr : f' < r) :
+    ∀ᶠ z in 𝓝[s \ {x}] x, slope f x z < r :=
+  hasDerivWithinAt_iff_tendsto_slope.1 hf (IsOpen.mem_nhds isOpen_Iio hr)
+#align has_deriv_within_at.limsup_slope_le HasDerivWithinAt.limsup_slope_le
+
+theorem HasDerivWithinAt.limsup_slope_le' (hf : HasDerivWithinAt f f' s x) (hs : x ∉ s)
+    (hr : f' < r) : ∀ᶠ z in 𝓝[s] x, slope f x z < r :=
+  (hasDerivWithinAt_iff_tendsto_slope' hs).1 hf (IsOpen.mem_nhds isOpen_Iio hr)
+#align has_deriv_within_at.limsup_slope_le' HasDerivWithinAt.limsup_slope_le'
+
+theorem HasDerivWithinAt.liminf_right_slope_le (hf : HasDerivWithinAt f f' (Ici x) x)
+    (hr : f' < r) : ∃ᶠ z in 𝓝[>] x, slope f x z < r :=
+  (hf.Ioi_of_Ici.limsup_slope_le' (lt_irrefl x) hr).frequently
+#align has_deriv_within_at.liminf_right_slope_le HasDerivWithinAt.liminf_right_slope_le
+
+end Real
+
+section RealSpace
+
+open Metric
+
+variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {f' : E} {s : Set ℝ}
+  {x r : ℝ}
+
+/-- If `f` has derivative `f'` within `s` at `x`, then for any `r > ‖f'‖` the ratio
+`‖f z - f x‖ / ‖z - x‖` is less than `r` in some neighborhood of `x` within `s`.
+In other words, the limit superior of this ratio as `z` tends to `x` along `s`
+is less than or equal to `‖f'‖`. -/
+theorem HasDerivWithinAt.limsup_norm_slope_le (hf : HasDerivWithinAt f f' s x) (hr : ‖f'‖ < r) :
+    ∀ᶠ z in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r := by
+  have hr₀ : 0 < r := lt_of_le_of_lt (norm_nonneg f') hr
+  have A : ∀ᶠ z in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
+    (hasDerivWithinAt_iff_tendsto_slope.1 hf).norm (IsOpen.mem_nhds isOpen_Iio hr)
+  have B : ∀ᶠ z in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
+    mem_of_superset self_mem_nhdsWithin (singleton_subset_iff.2 <| by simp [hr₀])
+  have C := mem_sup.2 ⟨A, B⟩
+  rw [← nhdsWithin_union, diff_union_self, nhdsWithin_union, mem_sup] at C
+  filter_upwards [C.1]
+  simp only [norm_smul, mem_Iio, norm_inv]
+  exact fun _ => id
+#align has_deriv_within_at.limsup_norm_slope_le HasDerivWithinAt.limsup_norm_slope_le
+
+/-- If `f` has derivative `f'` within `s` at `x`, then for any `r > ‖f'‖` the ratio
+`(‖f z‖ - ‖f x‖) / ‖z - x‖` is less than `r` in some neighborhood of `x` within `s`.
+In other words, the limit superior of this ratio as `z` tends to `x` along `s`
+is less than or equal to `‖f'‖`.
+
+This lemma is a weaker version of `HasDerivWithinAt.limsup_norm_slope_le`
+where `‖f z‖ - ‖f x‖` is replaced by `‖f z - f x‖`. -/
+theorem HasDerivWithinAt.limsup_slope_norm_le (hf : HasDerivWithinAt f f' s x) (hr : ‖f'‖ < r) :
+    ∀ᶠ z in 𝓝[s] x, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r := by
+  apply (hf.limsup_norm_slope_le hr).mono
+  intro z hz
+  refine' lt_of_le_of_lt (mul_le_mul_of_nonneg_left (norm_sub_norm_le _ _) _) hz
+  exact inv_nonneg.2 (norm_nonneg _)
+#align has_deriv_within_at.limsup_slope_norm_le HasDerivWithinAt.limsup_slope_norm_le
+
+/-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ‖f'‖` the ratio
+`‖f z - f x‖ / ‖z - x‖` is frequently less than `r` as `z → x+0`.
+In other words, the limit inferior of this ratio as `z` tends to `x+0`
+is less than or equal to `‖f'‖`. See also `HasDerivWithinAt.limsup_norm_slope_le`
+for a stronger version using limit superior and any set `s`. -/
+theorem HasDerivWithinAt.liminf_right_norm_slope_le (hf : HasDerivWithinAt f f' (Ici x) x)
+    (hr : ‖f'‖ < r) : ∃ᶠ z in 𝓝[>] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r :=
+  (hf.Ioi_of_Ici.limsup_norm_slope_le hr).frequently
+#align has_deriv_within_at.liminf_right_norm_slope_le HasDerivWithinAt.liminf_right_norm_slope_le
+
+/-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ‖f'‖` the ratio
+`(‖f z‖ - ‖f x‖) / (z - x)` is frequently less than `r` as `z → x+0`.
+In other words, the limit inferior of this ratio as `z` tends to `x+0`
+is less than or equal to `‖f'‖`.
+
+See also
+
+* `HasDerivWithinAt.limsup_norm_slope_le` for a stronger version using
+  limit superior and any set `s`;
+* `HasDerivWithinAt.liminf_right_norm_slope_le` for a stronger version using
+  `‖f z - f xp‖` instead of `‖f z‖ - ‖f x‖`. -/
+theorem HasDerivWithinAt.liminf_right_slope_norm_le (hf : HasDerivWithinAt f f' (Ici x) x)
+    (hr : ‖f'‖ < r) : ∃ᶠ z in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r := by
+  have := (hf.Ioi_of_Ici.limsup_slope_norm_le hr).frequently
+  refine this.mp (Eventually.mono self_mem_nhdsWithin fun z hxz hz ↦ ?_)
+  rwa [Real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz
+#align has_deriv_within_at.liminf_right_slope_norm_le HasDerivWithinAt.liminf_right_slope_norm_le
+
+end RealSpace