# Documentation

Mathlib.Analysis.Calculus.Dslope

# 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} [] (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.

Instances For
@[simp]
theorem dslope_same {𝕜 : Type u_1} {E : Type u_2} [] (f : 𝕜E) (a : 𝕜) :
dslope f a a = deriv f a
theorem dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [] {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} [] {F : Type u_3} [] (f : E →L[𝕜] F) (g : 𝕜E) (a : 𝕜) (b : 𝕜) (H : a = b) :
dslope (f g) a b = f (dslope g a b)
theorem eqOn_dslope_slope {𝕜 : Type u_1} {E : Type u_2} [] (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} [] {a : 𝕜} {b : 𝕜} (f : 𝕜E) (h : b a) :
theorem dslope_eventuallyEq_slope_punctured_nhds {𝕜 : Type u_1} {E : Type u_2} [] {a : 𝕜} (f : 𝕜E) :
@[simp]
theorem sub_smul_dslope {𝕜 : Type u_1} {E : Type u_2} [] (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} [] {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} [] (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} [] [] (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} [] {f : 𝕜E} {a : 𝕜} :
theorem ContinuousWithinAt.of_dslope {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {b : 𝕜} {s : Set 𝕜} (h : ContinuousWithinAt (dslope f a) s b) :
theorem ContinuousAt.of_dslope {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {b : 𝕜} (h : ContinuousAt (dslope f a) b) :
theorem ContinuousOn.of_dslope {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {s : Set 𝕜} (h : ContinuousOn (dslope f a) s) :
theorem continuousWithinAt_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {b : 𝕜} {s : Set 𝕜} (h : b a) :
theorem continuousAt_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {b : 𝕜} (h : b a) :
theorem continuousOn_dslope {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {s : Set 𝕜} (h : s nhds a) :
theorem DifferentiableWithinAt.of_dslope {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {b : 𝕜} {s : Set 𝕜} (h : DifferentiableWithinAt 𝕜 (dslope f a) s b) :
theorem DifferentiableAt.of_dslope {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {b : 𝕜} (h : DifferentiableAt 𝕜 (dslope f a) b) :
theorem DifferentiableOn.of_dslope {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {s : Set 𝕜} (h : DifferentiableOn 𝕜 (dslope f a) s) :
theorem differentiableWithinAt_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {b : 𝕜} {s : Set 𝕜} (h : b a) :
theorem differentiableOn_dslope_of_nmem {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {s : Set 𝕜} (h : ¬a s) :
theorem differentiableAt_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [] {f : 𝕜E} {a : 𝕜} {b : 𝕜} (h : b a) :