19.3 Derivatives

　今回は微分法です．

# diffl;;
val it : thm =
|- !f x l.
(f diffl l) x <=>
((\h. (f (x + h) - f x) / h) tends_real_real l) (&0)

イプシロンデルタでは

# REWRITE_RULE[LIM; REAL_SUB_RZERO] diffl;;
val it : thm =
|- !f x l.
(f diffl l) x <=>
(!e. &0 < e
==> (?d. &0 < d /\
(!x'. &0 < abs x' /\ abs x' < d
==> abs ((f (x + x') - f x) / x' - l) < e)))

見ての通り

(f diffl l)xは，関数fの点xにおける微分係数がlである

ということです．

# REWRITE_CONV[diffl]`( (\x. x pow 2) diffl &2*a ) a` ;;
val it : thm =
|- ((\x. x pow 2) diffl &2 * a) a <=>
((\h. ((a + h) pow 2 - a pow 2) / h) tends_real_real &2 * a) (&0)

性質も

# DIFF_ADD;;
val it : thm =
|- !f g l m x.
(f diffl l) x /\ (g diffl m) x ==> *1 diffl l * m) x

# DIFF_CONST;;
val it : thm = |- !k x. *2 x
# DIFF_XM1;;
val it : thm = |- !x. ~(x = &0) ==> *3 x
# DIFF_INV;;
val it : thm =
|- !f l x.
(f diffl l) x /\ ~(f x = &0)
==> *4 diffl --(l / f x pow 2)) x

のようにthmとなっています．
　導関数を知るには(convではありませんが)DIFF_CONVがあります．

# DIFF_CONV `(\x:real. exp(a*x pow 2)*sin(b*x+c) )` ;;
val it : thm =
|- !x. *5 diffl
(exp (a * x pow 2) *
(&0 * x pow 2 + *6 * &1) * a)) *
sin (b * x + c) +
(cos (b * x + c) * *7 * exp (a * x pow 2))
x

*1:\x. f x + g x) diffl l + m) x # DIFF_SUB;; val it : thm = |- !f g l m x. (f diffl l) x /\ (g diffl m) x ==> ((\x. f x - g x) diffl l - m) x # DIFF_MUL;; val it : thm = |- !f g l m x. (f diffl l) x /\ (g diffl m) x ==> ((\x. f x * g x) diffl l * g x + m * f x) x # DIFF_DIV;; val it : thm = |- !f g l m. (f diffl l) x /\ (g diffl m) x /\ ~(g x = &0) ==> ((\x. f x / g x) diffl (l * g x - m * f x) / g x pow 2) x # DIFF_CHAIN;; val it : thm = |- !f g l m x. (f diffl l) (g x) /\ (g diffl m) x ==> ((\x. f (g x

*2:\x. k) diffl &0) x # DIFF_CMUL;; val it : thm = |- !f c l x. (f diffl l) x ==> ((\x. c * f x) diffl c * l) x # DIFF_NEG;; val it : thm = |- !f l x. (f diffl l) x ==> ((\x. --f x) diffl --l) x # DIFF_X;; val it : thm = |- !x. ((\x. x) diffl &1) x # DIFF_POW;; val it : thm = |- !n x. ((\x. x pow n) diffl &n * x pow (n - 1

*3:\x. inv x) diffl --(inv x pow 2

*4:\x. inv (f x

*5:\x. exp (a * x pow 2) * sin (b * x + c

*6:&2 * x pow (2 - 1

*7:&0 * x + &1 * b) + &0