Slope of a differentiable function

Given a function f : 𝕜 → E from a nontrivially normed field to a normed space over this field, dslope f a b is defined as slope f a b = (b - a)⁻¹ • (f b - f a) for a ≠ b and as deriv f a for a = b.

In this file we define dslope and prove some basic lemmas about its continuity and differentiability.

noncomputable def dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (a : 𝕜) : 𝕜 → E

dslope f a b is defined as slope f a b = (b - a)⁻¹ • (f b - f a) for a ≠ b and deriv f a for a = b.

Equations

• dslope f a = Function.update (slope f a) a (deriv f a)

@[simp]

theorem dslope_same {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (a : 𝕜) : dslope f a a = deriv f a

theorem dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a b : 𝕜} (f : 𝕜 → E) (h : b ≠ a) : dslope f a b = slope f a b

theorem ContinuousLinearMap.dslope_comp {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (g : 𝕜 → E) (a b : 𝕜) (H : a = b → DifferentiableAt 𝕜 g a) : dslope (⇑f ∘ g) a b = f (dslope g a b)

theorem eqOn_dslope_slope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (a : 𝕜) : Set.EqOn (dslope f a) (slope f a) {a}ᶜ

theorem dslope_eventuallyEq_slope_of_ne {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a b : 𝕜} (f : 𝕜 → E) (h : b ≠ a) : dslope f a =ᶠ[nhds b] slope f a

theorem dslope_eventuallyEq_slope_nhdsNE {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a : 𝕜} (f : 𝕜 → E) : dslope f a =ᶠ[nhdsWithin a {a}ᶜ] slope f a

@[simp]

theorem sub_smul_dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (a b : 𝕜) : (b - a) • dslope f a b = f b - f a

theorem dslope_sub_smul_of_ne {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a b : 𝕜} (f : 𝕜 → E) (h : b ≠ a) : dslope (fun (x : 𝕜) => (x - a) • f x) a b = f b

theorem eqOn_dslope_sub_smul {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (a : 𝕜) : Set.EqOn (dslope (fun (x : 𝕜) => (x - a) • f x) a) f {a}ᶜ

theorem dslope_sub_smul {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [DecidableEq 𝕜] (f : 𝕜 → E) (a : 𝕜) : dslope (fun (x : 𝕜) => (x - a) • f x) a = Function.update f a (deriv (fun (x : 𝕜) => (x - a) • f x) a)

@[simp]

theorem continuousAt_dslope_same {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} : ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a

theorem ContinuousWithinAt.of_dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} {s : Set 𝕜} (h : ContinuousWithinAt (dslope f a) s b) : ContinuousWithinAt f s b

theorem ContinuousAt.of_dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} (h : ContinuousAt (dslope f a) b) : ContinuousAt f b

theorem ContinuousOn.of_dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜} (h : ContinuousOn (dslope f a) s) : ContinuousOn f s

theorem continuousWithinAt_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} {s : Set 𝕜} (h : b ≠ a) : ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b

theorem continuousAt_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} (h : b ≠ a) : ContinuousAt (dslope f a) b ↔ ContinuousAt f b

theorem continuousOn_dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜} (h : s ∈ nhds a) : ContinuousOn (dslope f a) s ↔ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a

theorem DifferentiableWithinAt.of_dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} {s : Set 𝕜} (h : DifferentiableWithinAt 𝕜 (dslope f a) s b) : DifferentiableWithinAt 𝕜 f s b

theorem DifferentiableAt.of_dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} (h : DifferentiableAt 𝕜 (dslope f a) b) : DifferentiableAt 𝕜 f b

theorem DifferentiableOn.of_dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜} (h : DifferentiableOn 𝕜 (dslope f a) s) : DifferentiableOn 𝕜 f s

theorem differentiableWithinAt_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} {s : Set 𝕜} (h : b ≠ a) : DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b

theorem differentiableOn_dslope_of_notMem {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜} (h : a ∉ s) : DifferentiableOn 𝕜 (dslope f a) s ↔ DifferentiableOn 𝕜 f s

theorem differentiableAt_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜} (h : b ≠ a) : DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b

theorem sub_smul_dslope_of_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} (hf : f a = 0) (b : 𝕜) : (b - a) • dslope f a b = f b

theorem pow_sub_smul_iterate_dslope_of_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} (n : ℕ) (hf : ∀ k < n, (Function.swap dslope a)^[k] f a = 0) (b : 𝕜) : (b - a) ^ n • (Function.swap dslope a)^[n] f b = f b

theorem HasFPowerSeriesAt.dslope_fslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {p : FormalMultilinearSeries 𝕜 𝕜 E} {z₀ : 𝕜} (hp : HasFPowerSeriesAt f p z₀) : HasFPowerSeriesAt (dslope f z₀) p.fslope z₀

If f has power series p at z₀, then dslope f z₀ has power series p.fslope at z₀.

@[deprecated HasFPowerSeriesAt.dslope_fslope (since := "2026-09-30")]

theorem HasFPowerSeriesAt.has_fpower_series_dslope_fslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {p : FormalMultilinearSeries 𝕜 𝕜 E} {z₀ : 𝕜} (hp : HasFPowerSeriesAt f p z₀) : HasFPowerSeriesAt (dslope f z₀) p.fslope z₀

Alias of HasFPowerSeriesAt.dslope_fslope.

---

If f has power series p at z₀, then dslope f z₀ has power series p.fslope at z₀.

theorem AnalyticWithinAt.dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜} {z : 𝕜} (hf : AnalyticWithinAt 𝕜 f s z) (hz : z ≠ a) : AnalyticWithinAt 𝕜 (dslope f a) s z

Away from the base point a, the function dslope f a is analytic within s at z as soon as f is.

theorem AnalyticAt.dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z : 𝕜} (hf : AnalyticAt 𝕜 f z) (a : 𝕜) : AnalyticAt 𝕜 (dslope f a) z

If f is analytic at z, then so is dslope f a, for any base point a.

theorem AnalyticOn.dslope_of_notMem {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜} (hf : AnalyticOn 𝕜 f s) (ha : a ∉ s) : AnalyticOn 𝕜 (dslope f a) s

If f is analytic on s and the base point a does not lie in s, then dslope f a is analytic on s.

theorem AnalyticOn.dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜} (hf : AnalyticOn 𝕜 f s) (ha : s ∈ nhds a) : AnalyticOn 𝕜 (dslope f a) s

If f is analytic on a set s that is a neighbourhood of the base point a, then dslope f a is analytic on s.

theorem AnalyticOnNhd.dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {s : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f s) (a : 𝕜) : AnalyticOnNhd 𝕜 (dslope f a) s

If f is analytic on a neighbourhood of s, then so is dslope f a, for any base point a.