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
- dslope f a = function.update (slope f a) a (deriv f a)
@[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 : ๐) :
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) :
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) :
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 : ๐) :
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) :
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 : ๐) :
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 : ๐) :
@[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 : ๐} :
continuous_at (dslope f a) a โ differentiable_at ๐ f 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) :
continuous_within_at f 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) :
continuous_at f 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) :
continuous_on f 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) :
continuous_within_at (dslope f a) s b โ continuous_within_at f s b
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) :
continuous_at (dslope f a) b โ continuous_at f b
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) :
continuous_on (dslope f a) s โ continuous_on f s โง differentiable_at ๐ f 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) :
differentiable_within_at ๐ (dslope f a) s b โ differentiable_within_at ๐ f s b
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