mathlib documentation

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} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [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} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] (f : ๐•œ โ†’ E) (a : ๐•œ) :
dslope f a a = deriv f a
theorem dslope_of_ne {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {a b : ๐•œ} (f : ๐•œ โ†’ E) (h : b โ‰  a) :
dslope f a b = slope f a b
theorem continuous_linear_map.dslope_comp {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space ๐•œ F] (f : E โ†’L[๐•œ] F) (g : ๐•œ โ†’ E) (a b : ๐•œ) (H : a = b โ†’ differentiable_at ๐•œ g a) :
dslope (โ‡‘f โˆ˜ g) a b = โ‡‘f (dslope g a b)
theorem eq_on_dslope_slope {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] (f : ๐•œ โ†’ E) (a : ๐•œ) :
theorem dslope_eventually_eq_slope_of_ne {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {a b : ๐•œ} (f : ๐•œ โ†’ E) (h : b โ‰  a) :
theorem dslope_eventually_eq_slope_punctured_nhds {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {a : ๐•œ} (f : ๐•œ โ†’ E) :
@[simp]
theorem sub_smul_dslope {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ 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} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [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} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [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} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] [decidable_eq ๐•œ] (f : ๐•œ โ†’ E) (a : ๐•œ) :
dslope (ฮป (x : ๐•œ), (x - a) โ€ข f x) a = function.update f a (deriv (ฮป (x : ๐•œ), (x - a) โ€ข f x) a)
@[simp]
theorem continuous_at_dslope_same {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} :
theorem continuous_within_at.of_dslope {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a b : ๐•œ} {s : set ๐•œ} (h : continuous_within_at (dslope f a) s b) :
theorem continuous_at.of_dslope {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [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} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [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} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a b : ๐•œ} {s : set ๐•œ} (h : b โ‰  a) :
theorem continuous_at_dslope_of_ne {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a b : ๐•œ} (h : b โ‰  a) :
theorem continuous_on_dslope {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [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} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a b : ๐•œ} {s : set ๐•œ} (h : differentiable_within_at ๐•œ (dslope f a) s b) :
differentiable_within_at ๐•œ f s b
theorem differentiable_at.of_dslope {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a b : ๐•œ} (h : differentiable_at ๐•œ (dslope f a) b) :
differentiable_at ๐•œ f b
theorem differentiable_on.of_dslope {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {s : set ๐•œ} (h : differentiable_on ๐•œ (dslope f a) s) :
differentiable_on ๐•œ f s
theorem differentiable_within_at_dslope_of_ne {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a b : ๐•œ} {s : set ๐•œ} (h : b โ‰  a) :
theorem differentiable_on_dslope_of_nmem {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {s : set ๐•œ} (h : a โˆ‰ s) :
differentiable_on ๐•œ (dslope f a) s โ†” differentiable_on ๐•œ f s
theorem differentiable_at_dslope_of_ne {๐•œ : Type u_1} {E : Type u_2} [nontrivially_normed_field ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {f : ๐•œ โ†’ E} {a b : ๐•œ} (h : b โ‰  a) :
differentiable_at ๐•œ (dslope f a) b โ†” differentiable_at ๐•œ f b