# mathlibdocumentation

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} [normed_space ๐ 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
@[simp]
theorem dslope_same {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] (f : ๐ โ E) (a : ๐) :
a a = a
theorem dslope_of_ne {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {a b : ๐} (f : ๐ โ E) (h : b โ  a) :
a b = a b
theorem continuous_linear_map.dslope_comp {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {F : Type u_3} [normed_space ๐ F] (f : E โL[๐] F) (g : ๐ โ E) (a b : ๐) (H : a = b โ g a) :
dslope (โf โ g) a b = โf (dslope g a b)
theorem eq_on_dslope_slope {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] (f : ๐ โ E) (a : ๐) :
theorem dslope_eventually_eq_slope_of_ne {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {a b : ๐} (f : ๐ โ E) (h : b โ  a) :
theorem dslope_eventually_eq_slope_punctured_nhds {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {a : ๐} (f : ๐ โ E) :
@[simp]
theorem sub_smul_dslope {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] (f : ๐ โ E) (a b : ๐) :
(b - a) โข a b = f b - f a
theorem dslope_sub_smul_of_ne {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {a b : ๐} (f : ๐ โ E) (h : b โ  a) :
dslope (ฮป (x : ๐), (x - a) โข f x) a b = f b
theorem eq_on_dslope_sub_smul {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] (f : ๐ โ E) (a : ๐) :
set.eq_on (dslope (ฮป (x : ๐), (x - a) โข f x) a) f {a}แถ
theorem dslope_sub_smul {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] [decidable_eq ๐] (f : ๐ โ E) (a : ๐) :
dslope (ฮป (x : ๐), (x - a) โข f x) a = (deriv (ฮป (x : ๐), (x - a) โข f x) a)
@[simp]
theorem continuous_at_dslope_same {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a : ๐} :
theorem continuous_within_at.of_dslope {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a b : ๐} {s : set ๐} (h : s b) :
b
theorem continuous_at.of_dslope {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a b : ๐} (h : continuous_at (dslope f a) b) :
theorem continuous_on.of_dslope {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a : ๐} {s : set ๐} (h : continuous_on (dslope f a) s) :
theorem continuous_within_at_dslope_of_ne {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a b : ๐} {s : set ๐} (h : b โ  a) :
s b โ b
theorem continuous_at_dslope_of_ne {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a b : ๐} (h : b โ  a) :
theorem continuous_on_dslope {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a : ๐} {s : set ๐} (h : s โ nhds a) :
theorem differentiable_within_at.of_dslope {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a b : ๐} {s : set ๐} (h : (dslope f a) s b) :
f s b
theorem differentiable_at.of_dslope {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a b : ๐} (h : (dslope f a) b) :
f b
theorem differentiable_on.of_dslope {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a : ๐} {s : set ๐} (h : (dslope f a) s) :
f s
theorem differentiable_within_at_dslope_of_ne {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a b : ๐} {s : set ๐} (h : b โ  a) :
(dslope f a) s b โ f s b
theorem differentiable_on_dslope_of_nmem {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a : ๐} {s : set ๐} (h : a โ s) :
(dslope f a) s โ f s
theorem differentiable_at_dslope_of_ne {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {f : ๐ โ E} {a b : ๐} (h : b โ  a) :
(dslope f a) b โ f b