長めの例: 微分公式を組み合わせる

ここでは，関数

\[ f(x) = x^3 + 2x + 1 \]

が x = 5 で微分係数 77 を持つことを示します． 紙の計算では f'(x) = 3x^2 + 2 なので f'(5) = 77 です．

Lean では，HasDerivAt の証明を組み合わせて同じことを表します．

section PolynomialDerivativeExample

theorem cubicExample_hasDerivAt :
    HasDerivAt (fun x : ℝ => x ^ 3 + 2 * x + 1) (77 : ℝ) 5 := by
  have hpow : HasDerivAt (fun x : ℝ => x ^ 3) (3 * 5 ^ (3 - 1)) 5 := by
    simpa using (hasDerivAt_pow 3 (5 : ℝ))
  have hlin : HasDerivAt (fun x : ℝ => 2 * x) (2 * 1) 5 := by
    simpa using ((hasDerivAt_id (5 : ℝ)).const_mul (2 : ℝ))
  have h := (hpow.add hlin).add_const (1 : ℝ)
  have hcoeff : 3 * 5 ^ 2 + 2 = (77 : ℝ) := by
    calc
      (3 : ℝ) * 5 ^ 2 + 2 = 3 * 25 + 2 := by norm_num
      _ = 77 := by norm_num
  simpa [Pi.add_apply, hcoeff] using h

example : deriv (fun x : ℝ => x ^ 3 + 2 * x + 1) 5 = 77 := by
  exact cubicExample_hasDerivAt.deriv

end PolynomialDerivativeExample

この例では，次の補題を使っています．

• hasDerivAt_pow: 冪関数の微分
• hasDerivAt_id: 恒等関数の微分
• HasDerivAt.const_mul: 定数倍の微分
• HasDerivAt.add: 和の微分
• HasDerivAt.add_const: 定数を足しても微分係数は変わらない

最後は，Lean が持っている導関数の値を hcoeff で数値計算し， simpa [Pi.add_apply, hcoeff] using h で関数の表示と導関数の値を整理しています． hcoeff の中では calc を使い，

\[ 3 \cdot 5^2 + 2 = 3 \cdot 25 + 2 = 77 \]

という数値計算を段階的に書いています． convert を使うと，Mathlib のバージョンによっては型クラスインスタンスの等式まで 余分なゴールとして現れることがあるため，ここでは数値計算を明示的に分けています．

演習問題

x ↦ 3 * x ^ 2 の点 2 における微分係数を HasDerivAt で示してください．

example : HasDerivAt (fun x : ℝ => 3 * x ^ 2) (12 : ℝ) 2 := by
  -- `hasDerivAt_pow` と `.const_mul` を使う．
  -- 解答例:
  --   have hpow : HasDerivAt (fun x : ℝ => x ^ 2) (2 * 2 ^ (2 - 1)) 2 := by
  --     simpa using (hasDerivAt_pow 2 (2 : ℝ))
  --   have h := hpow.const_mul (3 : ℝ)
  --   have hcoeff : (3 : ℝ) * (2 * 2) = 12 := by
  --     calc
  --       (3 : ℝ) * (2 * 2) = 3 * 4 := by norm_num
  --       _ = 12 := by norm_num
  --   simpa [mul_assoc, hcoeff] using h
  sorry