# 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} [] [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
Instances For
@[simp]
theorem dslope_same {๐ : Type u_1} {E : Type u_2} [] [NormedSpace ๐ E] (f : ๐ โ E) (a : ๐) :
dslope f a a = deriv f a
theorem dslope_of_ne {๐ : Type u_1} {E : Type u_2} [] [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} [] [NormedSpace ๐ E] {F : Type u_3} [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} [] [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} [] [NormedSpace ๐ E] {a : ๐} {b : ๐} (f : ๐ โ E) (h : b โ  a) :
theorem dslope_eventuallyEq_slope_punctured_nhds {๐ : Type u_1} {E : Type u_2} [] [NormedSpace ๐ E] {a : ๐} (f : ๐ โ E) :
@[simp]
theorem sub_smul_dslope {๐ : Type u_1} {E : Type u_2} [] [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} [] [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} [] [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} [] [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} [] [NormedSpace ๐ E] {f : ๐ โ E} {a : ๐} :
theorem ContinuousWithinAt.of_dslope {๐ : Type u_1} {E : Type u_2} [] [NormedSpace ๐ E] {f : ๐ โ E} {a : ๐} {b : ๐} {s : Set ๐} (h : ContinuousWithinAt (dslope f a) s b) :
theorem ContinuousAt.of_dslope {๐ : Type u_1} {E : Type u_2} [] [NormedSpace ๐ E] {f : ๐ โ E} {a : ๐} {b : ๐} (h : ContinuousAt (dslope f a) b) :
theorem ContinuousOn.of_dslope {๐ : Type u_1} {E : Type u_2} [] [NormedSpace ๐ E] {f : ๐ โ E} {a : ๐} {s : Set ๐} (h : ContinuousOn (dslope f a) s) :
theorem continuousWithinAt_dslope_of_ne {๐ : Type u_1} {E : Type u_2} [] [NormedSpace ๐ E] {f : ๐ โ E} {a : ๐} {b : ๐} {s : Set ๐} (h : b โ  a) :
theorem continuousAt_dslope_of_ne {๐ : Type u_1} {E : Type u_2} [] [NormedSpace ๐ E] {f : ๐ โ E} {a : ๐} {b : ๐} (h : b โ  a) :
theorem continuousOn_dslope {๐ : Type u_1} {E : Type u_2} [] [NormedSpace ๐ E] {f : ๐ โ E} {a : ๐} {s : Set ๐} (h : s โ nhds a) :
theorem DifferentiableWithinAt.of_dslope {๐ : Type u_1} {E : Type u_2} [] [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} [] [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} [] [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} [] [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_nmem {๐ : Type u_1} {E : Type u_2} [] [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} [] [NormedSpace ๐ E] {f : ๐ โ E} {a : ๐} {b : ๐} (h : b โ  a) :
DifferentiableAt ๐ (dslope f a) b โ DifferentiableAt ๐ f b