Documentation

Mathlib.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} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ 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
Instances For
    @[simp]
    theorem dslope_same {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] (f : ๐•œ โ†’ E) (a : ๐•œ) :
    dslope f a a = deriv f a
    theorem dslope_of_ne {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {a : ๐•œ} {b : ๐•œ} (f : ๐•œ โ†’ E) (h : b โ‰  a) :
    dslope f a b = slope f a b
    theorem ContinuousLinearMap.dslope_comp {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] (f : E โ†’L[๐•œ] F) (g : ๐•œ โ†’ E) (a : ๐•œ) (b : ๐•œ) (H : a = b โ†’ DifferentiableAt ๐•œ g a) :
    dslope (โ‡‘f โˆ˜ g) a b = f (dslope g a b)
    theorem eqOn_dslope_slope {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] (f : ๐•œ โ†’ E) (a : ๐•œ) :
    Set.EqOn (dslope f a) (slope f a) {a}แถœ
    theorem dslope_eventuallyEq_slope_of_ne {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {a : ๐•œ} {b : ๐•œ} (f : ๐•œ โ†’ E) (h : b โ‰  a) :
    (nhds b).EventuallyEq (dslope f a) (slope f a)
    theorem dslope_eventuallyEq_slope_punctured_nhds {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {a : ๐•œ} (f : ๐•œ โ†’ E) :
    (nhdsWithin a {a}แถœ).EventuallyEq (dslope f a) (slope f a)
    @[simp]
    theorem sub_smul_dslope {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ 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} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {a : ๐•œ} {b : ๐•œ} (f : ๐•œ โ†’ E) (h : b โ‰  a) :
    dslope (fun (x : ๐•œ) => (x - a) โ€ข f x) a b = f b
    theorem eqOn_dslope_sub_smul {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] (f : ๐•œ โ†’ E) (a : ๐•œ) :
    Set.EqOn (dslope (fun (x : ๐•œ) => (x - a) โ€ข f x) a) f {a}แถœ
    theorem dslope_sub_smul {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [DecidableEq ๐•œ] (f : ๐•œ โ†’ E) (a : ๐•œ) :
    dslope (fun (x : ๐•œ) => (x - a) โ€ข f x) a = Function.update f a (deriv (fun (x : ๐•œ) => (x - a) โ€ข f x) a)
    @[simp]
    theorem continuousAt_dslope_same {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} :
    theorem ContinuousWithinAt.of_dslope {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {b : ๐•œ} {s : Set ๐•œ} (h : ContinuousWithinAt (dslope f a) s b) :
    theorem ContinuousAt.of_dslope {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {b : ๐•œ} (h : ContinuousAt (dslope f a) b) :
    theorem ContinuousOn.of_dslope {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {s : Set ๐•œ} (h : ContinuousOn (dslope f a) s) :
    theorem continuousWithinAt_dslope_of_ne {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {b : ๐•œ} {s : Set ๐•œ} (h : b โ‰  a) :
    theorem continuousAt_dslope_of_ne {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {b : ๐•œ} (h : b โ‰  a) :
    theorem continuousOn_dslope {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {s : Set ๐•œ} (h : s โˆˆ nhds a) :
    theorem DifferentiableWithinAt.of_dslope {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {b : ๐•œ} {s : Set ๐•œ} (h : DifferentiableWithinAt ๐•œ (dslope f a) s b) :
    DifferentiableWithinAt ๐•œ f s b
    theorem DifferentiableAt.of_dslope {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {b : ๐•œ} (h : DifferentiableAt ๐•œ (dslope f a) b) :
    DifferentiableAt ๐•œ f b
    theorem DifferentiableOn.of_dslope {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {s : Set ๐•œ} (h : DifferentiableOn ๐•œ (dslope f a) s) :
    DifferentiableOn ๐•œ f s
    theorem differentiableWithinAt_dslope_of_ne {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {b : ๐•œ} {s : Set ๐•œ} (h : b โ‰  a) :
    DifferentiableWithinAt ๐•œ (dslope f a) s b โ†” DifferentiableWithinAt ๐•œ f s b
    theorem differentiableOn_dslope_of_nmem {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {s : Set ๐•œ} (h : a โˆ‰ s) :
    DifferentiableOn ๐•œ (dslope f a) s โ†” DifferentiableOn ๐•œ f s
    theorem differentiableAt_dslope_of_ne {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {a : ๐•œ} {b : ๐•œ} (h : b โ‰  a) :
    DifferentiableAt ๐•œ (dslope f a) b โ†” DifferentiableAt ๐•œ f b