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
- 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