# mathlibdocumentation

analysis.calculus.dslope

# Slope of a differentiable function #

Given a function f : 𝕜 → E from a nondiscrete 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_group E] [ 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_group E] [ E] (f : 𝕜 → E) (a : 𝕜) :
a a = a
theorem dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ 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_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (g : 𝕜 → E) (a b : 𝕜) (H : a = b a) :
dslope (f g) a b = f (dslope g a b)
theorem eq_on_dslope_slope {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (f : 𝕜 → E) (a : 𝕜) :
set.eq_on (dslope f a) (slope f a) {a}
theorem dslope_eventually_eq_slope_of_ne {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {a b : 𝕜} (f : 𝕜 → E) (h : b a) :
a =ᶠ[nhds b] a
theorem dslope_eventually_eq_slope_punctured_nhds {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {a : 𝕜} (f : 𝕜 → E) :
a =ᶠ[ {a}] a
@[simp]
theorem sub_smul_dslope {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ 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_group E] [ 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_group E] [ 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_group E] [ 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_group E] [ E] {f : 𝕜 → E} {a : 𝕜} :
theorem continuous_within_at.of_dslope {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : 𝕜 → E} {a b : 𝕜} {s : set 𝕜} (h : s b) :
b
theorem continuous_at.of_dslope {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ 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_group E] [ 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_group E] [ 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_group E] [ E] {f : 𝕜 → E} {a b : 𝕜} (h : b a) :
theorem continuous_on_dslope {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : 𝕜 → E} {a : 𝕜} {s : set 𝕜} (h : s nhds a) :
theorem differentiable_within_at.of_dslope {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : 𝕜 → E} {a b : 𝕜} {s : set 𝕜} (h : (dslope f a) s b) :
b
theorem differentiable_at.of_dslope {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : 𝕜 → E} {a b : 𝕜} (h : (dslope f a) b) :
b
theorem differentiable_on.of_dslope {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : 𝕜 → E} {a : 𝕜} {s : set 𝕜} (h : (dslope f a) s) :
s
theorem differentiable_within_at_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : 𝕜 → E} {a b : 𝕜} {s : set 𝕜} (h : b a) :
(dslope f a) s b b
theorem differentiable_on_dslope_of_nmem {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : 𝕜 → E} {a : 𝕜} {s : set 𝕜} (h : a s) :
(dslope f a) s s
theorem differentiable_at_dslope_of_ne {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : 𝕜 → E} {a b : 𝕜} (h : b a) :
(dslope f a) b b