Chapter 04: 微分

Mathlib における基本的な微分を扱います．

参考:

• Mathematics in Lean, 12. Differential Calculus: https://leanprover-community.github.io/mathematics_in_lean/C12_Differential_Calculus.html

実数値関数の初等微分から，ノルム空間上の Fréchet 微分までが説明されています．

微分に関する主な述語・関数は次の通りです．

• HasDerivAt f f' x: 1 変数関数 f が点 x で微分係数 f' を持つ．
• DifferentiableAt ℝ f x: f が点 x で微分可能である．
• deriv f x: f の点 x における微分係数．微分不能な点では 0 と定義される．
• HasFDerivAt f f' x: ノルム空間上の Fréchet 微分．
• fderiv 𝕜 f x: Fréchet 微分としての導関数．

import Mathlib

namespace PracticeChapter04

noncomputable section

open Set Filter
open scoped Topology