mathlib3 documentation

analysis.calculus.dslope

Slope of a differentiable function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : π•œ) :
set.eq_on (dslope f a) (slope f a) {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) :
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