微分の計算規則

和，積，合成などの微分公式は，HasDerivAt 版，DifferentiableAt 版，deriv 版など複数の形で用意されています． まずは補題の型を #check で確認し，必要な仮定を揃えます．

#check HasDerivAt.add
#check HasDerivAt.mul
#check HasDerivAt.comp
#check deriv_add
#check deriv_mul

section DerivativeRules

example {f g : ℝ → ℝ} {x : ℝ}
    (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    deriv (fun y => f y + g y) x = deriv f x + deriv g x := by
  exact deriv_add hf hg

example {f g : ℝ → ℝ} {x : ℝ}
    (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    deriv (fun y => f y * g y) x = deriv f x * g x + f x * deriv g x := by
  exact deriv_mul hf hg

example {f g : ℝ → ℝ} {x a b : ℝ}
    (hf : HasDerivAt f a x) (hg : HasDerivAt g b x) :
    HasDerivAt (fun y => f y + g y) (a + b) x := by
  exact hf.add hg

end DerivativeRules

演習問題

積の微分公式を使って，f * g の導関数を表してください．

example {f g : ℝ → ℝ} {x : ℝ}
    (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    deriv (fun y => f y * g y) x = deriv f x * g x + f x * deriv g x := by
  -- ヒント: `exact deriv_mul hf hg`
  -- 解答例: exact deriv_mul hf hg
  sorry