Mathlib における微分の形式化¶
Mathlib の微分は，1 変数実関数の極限
から直接始めるのではなく，ノルム空間上の Fréchet 微分を中心に実装されています．
基礎になる型は，ノルム体 𝕜 上のノルム空間 E，F と，関数 f : E → F です．
点 x : E における微分は数ではなく，連続線形写像 f' : E →L[𝕜] F として表されます．
数学的には，HasFDerivAt f f' x は
という一次近似を表します．
Lean ではこの o はフィルター 𝓝 x に沿った漸近記法として表されます．
Mathlib の定義ファイルでは，さらに一般に HasFDerivAtFilter が用意されており，
通常の点での微分 HasFDerivAt，集合内での微分 HasFDerivWithinAt，逆関数定理などで使う strict derivative HasStrictFDerivAt が，
どのフィルターに沿って同じ一次近似を見るかの違いとして定義されています．
DifferentiableAt 𝕜 f x は「そのような連続線形写像 f' が存在する」という述語です．
一方 fderiv 𝕜 f x は導関数を値として返す関数です．
導関数が存在すればその値を返し，存在しなければ 0 に定義されます．
そのため，証明ではまず HasFDerivAt や HasDerivAt を作り，最後に .fderiv や .deriv で値としての導関数へ移ります．
1 変数の HasDerivAt f f' x は，この Fréchet 微分の特殊化です．
関数 f : 𝕜 → F の微分係数 f' : F を，h ↦ h • f' という連続線形写像に対応させて HasFDerivAt に戻しています．
特に f : ℝ → ℝ なら，いつもの微分係数は実数として現れます．
deriv f x は fderiv 𝕜 f x を方向 1 に評価したものです．
前半では HasDerivAt，deriv，Rolle の定理や平均値の定理を扱い，
後半ではノルム空間，連続線形写像 E →L[𝕜] F，漸近記法 =O・=o，HasFDerivAt，ContDiff，逆関数定理へ進みます．
漸近記法 =o を読む¶
Mathlib では，Landau の little-o 記法を
と書きます．
これは「フィルター l に沿って，f は g より十分小さい」という意味です．
たとえば l = 𝓝 x なら，変数が点 x に近づくときの漸近的な大小を表しています．
Mathlib のソースでは，次のように定義されています．
irreducible_def IsLittleO (l : Filter α) (f : α → E) (g : α → F) : Prop :=
∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
notation:100 f " =o[" l "] " g:100 => IsLittleO l f g
theorem isLittleO_iff :
f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖
最後の isLittleO_iff が，数学的な読み方に一番近いです．
任意の正の定数 c に対して，l に沿って十分近いところでは
が成り立つ，という意味です．
つまり，f は g の任意に小さい定数倍で抑えられるほど小さい，ということです．
分母が 0 になる点を避けて直感的に書けば，‖f x‖ / ‖g x‖ → 0 です．
微分で出てくる
は，x' → x のとき，一次近似
からの誤差が，変位 x' - x に比べて高次の微小量であることを表しています．
これが「f' が点 x での微分である」という条件です．
=O は「ある定数倍で抑えられる」という有界な大小関係ですが，
=o は「任意に小さい定数倍で抑えられる」という，より強い条件です．
HasDerivAt と DifferentiableAt の定義を読む¶
1 変数の微分係数 HasDerivAt f f' x は，Mathlib のソースでは次のように定義されています．
def HasDerivAtFilter (f : 𝕜 → F) (f' : F) (L : Filter (𝕜 × 𝕜)) :=
HasFDerivAtFilter f (toSpanSingleton 𝕜 f') L
def HasDerivAt (f : 𝕜 → F) (f' : F) (x : 𝕜) :=
HasDerivAtFilter f f' (𝓝 x ×ˢ pure x)
ここで toSpanSingleton 𝕜 f' は，ベクトル f' : F を
h ↦ h • f' という連続線形写像 𝕜 →L[𝕜] F に変換するものです．
したがって数学的には，HasDerivAt f f' x は
という一次近似を表します．
特に f : ℝ → ℝ の場合，これは通常の
という微分係数の定義と対応します．
一方，DifferentiableAt は微分係数そのものを指定せず，「ある Fréchet 微分が存在する」と定義されています．
def HasFDerivAt (f : E → F) (f' : E →L[𝕜] F) (x : E) :=
HasFDerivAtFilter f f' (𝓝 x ×ˢ pure x)
def DifferentiableAt (f : E → F) (x : E) :=
∃ f' : E →L[𝕜] F, HasFDerivAt f f' x
つまり DifferentiableAt 𝕜 f x は，点 x の近くで
を満たす連続線形写像 f' : E →L[𝕜] F が存在する，という命題です．
HasDerivAt は微分係数の値まで指定する述語，DifferentiableAt は値を指定せず存在だけを主張する述語，と読むと使い分けやすいです．
#check HasFDerivAtFilter
#check HasFDerivAt
#check HasDerivAtFilter
#check HasDerivAt
#check fderiv
#check deriv
#check Asymptotics.IsLittleO
#check Asymptotics.isLittleO_iff
section DifferentialDefinitions
open Asymptotics
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E F : Type*}
variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable [NormedAddCommGroup F] [NormedSpace 𝕜 F]
example {f : E → F} {f' : E →L[𝕜] F} {x : E} :
HasFDerivAt f f' x ↔
(fun x' => f x' - f x - f' (x' - x)) =o[𝓝 x] (fun x' => x' - x) := by
exact hasFDerivAt_iff_isLittleO
example {f : E → F} {f' : E →L[𝕜] F} {x : E} :
HasFDerivAt f f' x ↔
Filter.Tendsto
(fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖)
(𝓝 x)
(𝓝 0) := by
exact hasFDerivAt_iff_tendsto
example {f : 𝕜 → F} {f' : F} {x : 𝕜} :
HasDerivAt f f' x ↔
(fun x' => f x' - f x - (x' - x) • f') =o[𝓝 x] (fun x' => x' - x) := by
exact hasDerivAt_iff_isLittleO
example {f : 𝕜 → F} {x : 𝕜} : deriv f x = (fderiv 𝕜 f x) 1 := by
rfl
end DifferentialDefinitions