実数値関数の微分

実数から実数への関数では，点での微分係数を HasDerivAt で表します． 微分係数を明示しない場合は DifferentiableAt ℝ を使います．

#check HasDerivAt
#check DifferentiableAt
#check deriv

section RealDerivatives

open Real

example : HasDerivAt sin 1 0 := by
  simpa using hasDerivAt_sin 0

example (x : ℝ) : DifferentiableAt ℝ sin x := by
  exact (hasDerivAt_sin x).differentiableAt

example {f : ℝ → ℝ} {x a : ℝ} (h : HasDerivAt f a x) : deriv f x = a := by
  exact h.deriv

example {f : ℝ → ℝ} {x : ℝ} (h : ¬ DifferentiableAt ℝ f x) : deriv f x = 0 := by
  exact deriv_zero_of_not_differentiableAt h

example : deriv (fun x : ℝ => x ^ 5) 6 = 5 * 6 ^ 4 := by
  calc
    deriv (fun x : ℝ => x ^ 5) 6 = 5 * 6 ^ (5 - 1) := by
      exact (hasDerivAt_pow 5 (6 : ℝ)).deriv
    _ = 5 * 6 ^ 4 := by norm_num

example : deriv sin π = -1 := by
  simp

end RealDerivatives

deriv f x は，任意の関数 f : ℝ → ℝ と点 x に対して定義されています． ただし，微分可能でない点では値が 0 になります． そのため，定理を使うときには HasDerivAt や DifferentiableAt の仮定が必要かを確認します．

微分の具体的な計算では，calc を使うと，紙の計算に近い形で式変形を読めます． たとえば上の例では，まず deriv_pow で

\[ \frac{d}{dx}x^5\bigg|_{x=6} = 5 \cdot 6^{5-1} \]

を得て，次に norm_num で \(5-1=4\) を計算しています． HasDerivAt や DifferentiableAt を作る部分は補題を使い， 導関数の係数や数値だけを calc で整理すると読みやすくなります．

演習問題

1. fun x : ℝ => x ^ 4 が任意の点で微分可能であることを示してください．

   example (x : ℝ) : DifferentiableAt ℝ (fun y : ℝ => y ^ 4) x := by
     -- `fun_prop` または `hasDerivAt_pow` から `.differentiableAt`．
     -- 解答例: fun_prop
     sorry
   

2. x^2 の点 3 における導関数が 6 であることを示してください．

   example : deriv (fun x : ℝ => x ^ 2) 3 = 6 := by
     -- `simp` と `norm_num` を試す．
     -- 解答例:
     --   calc
     --     deriv (fun x : ℝ => x ^ 2) 3 = 2 * 3 ^ (2 - 1) := by
     --       exact (hasDerivAt_pow 2 (3 : ℝ)).deriv
     --     _ = 6 := by norm_num
     sorry
   

3. HasDerivAt の証明から DifferentiableAt を取り出してください．

   example {f : ℝ → ℝ} {x a : ℝ} (h : HasDerivAt f a x) :
       DifferentiableAt ℝ f x := by
     -- ヒント: `exact h.differentiableAt`
     -- 解答例: exact h.differentiableAt
     sorry
   

4. deriv は微分不能な点で 0 と定義されることを，絶対値関数などで調べてください．

   -- 解答例: `deriv_zero_of_not_differentiableAt` が，
   -- 微分不能な点で `deriv` が 0 になることを述べます．
   #check deriv_zero_of_not_differentiableAt