11. 微分

ここから 解析学 の概念の形式化について考えていきましょう．この章では微分から始め，次の章では積分と測度論を取り上げます． Section 11.1 では，微積分の入門クラスでおなじみの実数から実数への関数設定に限定します． Section 11.2 では導関数の概念をより広い範囲で考えます．

11.1. 初等的な微分法

f を実数から実数への関数としたとき，ある1点における f の微分係数について話すのと導関数について話すのとでは違いがあります．Mathlibでは，前者の概念は次のように表現されます．

open Real

/-- The sin function has derivative 1 at 0. -/
example : HasDerivAt sin 1 0 := by simpa using hasDerivAt_sin 0

また，特定の点での微分を指定せずに f が微分可能であることも表現でき， DifferentiableAt ℝ と書きます．ここで， ℝ を明示的に指定しているのは，もう少し一般的な文脈において ℂ から ℂ までの関数について話す時に，実数的な意味で微分可能であることと，複素微分の意味で微分可能であることを区別できるようにしたいからです．

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

微分について言及するたびに微分可能性の証明をしなければならないのは不便です．そこで，Mathlibは関数 deriv f : ℝ → ℝ を提供しています．これは任意の関数 f : ℝ → ℝ に対して定義されますが， f が微分不可能な点では 0 をとるように定義されています．

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

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

もちろん deriv に関する補題で微分可能性の仮定を必要とするものはたくさんあります．例えば，微分可能性の仮定がない場合の次の補題の反例を考えてみるといいでしょう．

example {f g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    deriv (f + g) x = deriv f x + deriv g x :=
  deriv_add hf hg

しかし興味深いことに，関数が微分可能でない場合， deriv の値がデフォルトで0になるという事実を利用することで，微分可能性の仮定を回避できる文が存在します．そのため，以下の文の意味を理解するには deriv の正確な定義を知る必要があります．

example {f : ℝ → ℝ} {a : ℝ} (h : IsLocalMin f a) : deriv f a = 0 :=
  h.deriv_eq_zero

より奇妙に見えるでしょうが，微分可能性の仮定なしにロルの定理を示すことさえできます．

open Set

example {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
    ∃ c ∈ Ioo a b, deriv f c = 0 :=
  exists_deriv_eq_zero hab hfc hfI

もちろん，この技法は一般的な平均値の定理には通用しません．

example (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hf : ContinuousOn f (Icc a b))
    (hf' : DifferentiableOn ℝ f (Ioo a b)) : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) :=
  exists_deriv_eq_slope f hab hf hf'

Leanは simp タクティクを使って簡単な微分係数を自動的に計算することができます．

example : deriv (fun x : ℝ ↦ x ^ 5) 6 = 5 * 6 ^ 4 := by simp

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

11.2. ノルム空間の微分法

11.2.1. ノルム空間

微分は，方向と距離の両方を備えた ノルム線形空間 （normed vector space）の概念を用いることで ℝ を超えて一般化することができます．まず ノルム化された群 （normed group）の概念から始めましょう．これは以下の条件を満たす実数値ノルム関数を備えた加法可換群です．

variable {E : Type*} [NormedAddCommGroup E]

example (x : E) : 0 ≤ ‖x‖ :=
  norm_nonneg x

example {x : E} : ‖x‖ = 0 ↔ x = 0 :=
  norm_eq_zero

example (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ :=
  norm_add_le x y

すべてのノルム空間は距離関数 \(d(x, y) = \| x - y \|\) を持つ距離空間であり，したがって位相空間でもあります．LeanとMathlibはこの事実を知っています．

example : MetricSpace E := by infer_instance

example {X : Type*} [TopologicalSpace X] {f : X → E} (hf : Continuous f) :
    Continuous fun x ↦ ‖f x‖ :=
  hf.norm

線形代数からのコンセプトとノルムの概念を使うために， NormedAddGroup E の上に NormedSpace ℝ E という仮定を追加します．これは E が ℝ 上のベクトル空間であり，スカラー倍が以下の条件を満たすことを定めます．

variable [NormedSpace ℝ E]

example (a : ℝ) (x : E) : ‖a • x‖ = |a| * ‖x‖ :=
  norm_smul a x

完備なノルム空間は バナッハ空間 （Banach space）として知られています．すべての有限次元ベクトル空間は完備です．

example [FiniteDimensional ℝ E] : CompleteSpace E := by infer_instance

これまでの例はすべてベースの体として実数を使いました．より一般的には，任意の 非自明なノルム化された体 （nontrivially normed field）上のベクトル空間を使って微積分を理解することができます．これは乗法的ですべての要素のノルムが0か1ではない（つまり，ノルムが1より大きい要素が存在する）という性質を持つ実数値ノルムを備えた体です．

example (𝕜 : Type*) [NontriviallyNormedField 𝕜] (x y : 𝕜) : ‖x * y‖ = ‖x‖ * ‖y‖ :=
  norm_mul x y

example (𝕜 : Type*) [NontriviallyNormedField 𝕜] : ∃ x : 𝕜, 1 < ‖x‖ :=
  NormedField.exists_one_lt_norm 𝕜

非自明なノルム化された体上の有限次元ベクトル空間はその体自体が完備である場合に限り完備です．

example (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] : CompleteSpace E :=
  FiniteDimensional.complete 𝕜 E

11.2.2. 連続線形写像

次にノルム空間の圏における射，つまり連続線形写像について説明します．Mathlibでは，ノルム空間 E と F の間の 𝕜 線形連続写像の型を E →L[𝕜] F と表記します．これらは 束縛写像 （bundled maps）として実装されます．束縛写像とは，この型の要素が関数そのものと線形で連続であるという性質を含む構造を持つことを意味します．Leanは連続線形写像を関数として扱えるように型強制を備えています．

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]

example : E →L[𝕜] E :=
  ContinuousLinearMap.id 𝕜 E

example (f : E →L[𝕜] F) : E → F :=
  f

example (f : E →L[𝕜] F) : Continuous f :=
  f.cont

example (f : E →L[𝕜] F) (x y : E) : f (x + y) = f x + f y :=
  f.map_add x y

example (f : E →L[𝕜] F) (a : 𝕜) (x : E) : f (a • x) = a • f x :=
  f.map_smul a x

連続線形写像は以下の性質で特徴づけられる作用素ノルムを持ちます．

variable (f : E →L[𝕜] F)

example (x : E) : ‖f x‖ ≤ ‖f‖ * ‖x‖ :=
  f.le_opNorm x

example {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ x, ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M :=
  f.opNorm_le_bound hMp hM

また束縛された連続線形 同型 （isomorphism）という概念が存在します．この型は E ≃L[𝕜] F です．

発展的な演習として，一様有界性原理としても知られているバナッハ-シュタインハウスの定理を証明してみましょう．この原理はバナッハ空間からノルム空間への連続線形写像の族が点ごとに有界であれば，これらの線形写像のノルムは一様に有界であることを述べています．この証明の主成分はベールの定理 nonempty_interior_of_iUnion_of_closed です．（位相の章でこれを証明しました．）それ以外の材料として continuous_linear_map.opNorm_le_of_shell と interior_subset ， interior_iInter_subset ， isClosed_le が含まれます．

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]

open Metric

example {ι : Type*} [CompleteSpace E] {g : ι → E →L[𝕜] F} (h : ∀ x, ∃ C, ∀ i, ‖g i x‖ ≤ C) :
    ∃ C', ∀ i, ‖g i‖ ≤ C' := by
  -- sequence of subsets consisting of those `x : E` with norms `‖g i x‖` bounded by `n`
  let e : ℕ → Set E := fun n ↦ ⋂ i : ι, { x : E | ‖g i x‖ ≤ n }
  -- each of these sets is closed
  have hc : ∀ n : ℕ, IsClosed (e n)
  sorry
  -- the union is the entire space; this is where we use `h`
  have hU : (⋃ n : ℕ, e n) = univ
  sorry
  /- apply the Baire category theorem to conclude that for some `m : ℕ`,
       `e m` contains some `x` -/
  obtain ⟨m, x, hx⟩ : ∃ m, ∃ x, x ∈ interior (e m) := sorry
  obtain ⟨ε, ε_pos, hε⟩ : ∃ ε > 0, ball x ε ⊆ interior (e m) := sorry
  obtain ⟨k, hk⟩ : ∃ k : 𝕜, 1 < ‖k‖ := sorry
  -- show all elements in the ball have norm bounded by `m` after applying any `g i`
  have real_norm_le : ∀ z ∈ ball x ε, ∀ (i : ι), ‖g i z‖ ≤ m
  sorry
  have εk_pos : 0 < ε / ‖k‖ := sorry
  refine ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.opNorm_le_of_shell ε_pos ?_ hk ?_⟩
  sorry
  sorry

11.2.3. 漸近比較

微分可能性の定義には漸近比較も必要です．Mathlibにはビッグオーとリトルオーの関係をカバーする広範なライブラリがあり，その定義を以下に示されるものです． asymptotics 名前空間を開くと，対応する表記法を使うことができます．ここでは微分可能性を定義するためにリトルオーのみを使用します．

open Asymptotics

example {α : Type*} {E : Type*} [NormedGroup E] {F : Type*} [NormedGroup F] (c : ℝ)
    (l : Filter α) (f : α → E) (g : α → F) : IsBigOWith c l f g ↔ ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
  isBigOWith_iff

example {α : Type*} {E : Type*} [NormedGroup E] {F : Type*} [NormedGroup F]
    (l : Filter α) (f : α → E) (g : α → F) : f =O[l] g ↔ ∃ C, IsBigOWith C l f g :=
  isBigO_iff_isBigOWith

example {α : Type*} {E : Type*} [NormedGroup E] {F : Type*} [NormedGroup F]
    (l : Filter α) (f : α → E) (g : α → F) : f =o[l] g ↔ ∀ C > 0, IsBigOWith C l f g :=
  isLittleO_iff_forall_isBigOWith

example {α : Type*} {E : Type*} [NormedAddCommGroup E] (l : Filter α) (f g : α → E) :
    f ~[l] g ↔ (f - g) =o[l] g :=
  Iff.rfl

11.2.4. 微分可能性

これでノルム空間のあいだの微分可能な関数について議論する準備が整いました．初等的な一次元の場合になぞらえて，Mathlibでは HasFDerivAt という述語と fderiv という関数と定義しています．ここで f は フレシェ （Fréchet）を表します．

open Topology

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {F : Type*} [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₀ :=
  hasFDerivAtFilter_iff_isLittleO ..

example (f : E → F) (f' : E →L[𝕜] F) (x₀ : E) (hff' : HasFDerivAt f f' x₀) : fderiv 𝕜 f x₀ = f' :=
  hff'.fderiv

またMathlibには，多重線形写像 E [×n]→L[𝕜] F 型で値をとる反復微分や，連続微分関数も存在します．型 WithTop ℕ は ℕ にすべての自然数より大きい要素 ⊤ を加えたものです．つまり関数 \(\mathcal{C}^\infty\) は ContDiff 𝕜 ⊤ f を満たす関数 f です．

example (n : ℕ) (f : E → F) : E → E[×n]→L[𝕜] F :=
  iteratedFDeriv 𝕜 n f

example (n : WithTop ℕ) {f : E → F} :
    ContDiff 𝕜 n f ↔
      (∀ m : ℕ, (m : WithTop ℕ) ≤ n → Continuous fun x ↦ iteratedFDeriv 𝕜 m f x) ∧
        ∀ m : ℕ, (m : WithTop ℕ) < n → Differentiable 𝕜 fun x ↦ iteratedFDeriv 𝕜 m f x :=
  contDiff_iff_continuous_differentiable

より狭義な微分可能性の概念で HasStrictFDerivAt と呼ばれるものがあります．これはMathlibにある逆関数定理と陰関数定理の記述で使われています． ℝ もしくは ℂ 上の連続微分可能な関数は狭義微分可能です．

example {𝕂 : Type*} [RCLike 𝕂] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type*}
    [NormedAddCommGroup F] [NormedSpace 𝕂 F] {f : E → F} {x : E} {n : WithTop ℕ}
    (hf : ContDiffAt 𝕂 n f x) (hn : 1 ≤ n) : HasStrictFDerivAt f (fderiv 𝕂 f x) x :=
  hf.hasStrictFDerivAt hn

局所的な逆関数定理は，ある関数から逆関数を生成する操作と，その関数がある点 a において狭義微分可能であり，その導関数と同型であるという仮定を用いて述べられます．

以下の最初の例は，この局所的な逆関数を求めるためのものです．その次の例はこれが左右どちらからも局所的な逆であることを確かめ，そして狭義微分可能であることを述べています．

section LocalInverse
variable [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E}

example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) : F → E :=
  HasStrictFDerivAt.localInverse f f' a hf

example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ∀ᶠ x in 𝓝 a, hf.localInverse f f' a (f x) = x :=
  hf.eventually_left_inverse

example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ∀ᶠ x in 𝓝 (f a), f (hf.localInverse f f' a x) = x :=
  hf.eventually_right_inverse

example {f : E → F} {f' : E ≃L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (f'.symm : F →L[𝕜] E) (f a) :=
  HasStrictFDerivAt.to_localInverse hf

end LocalInverse

以上，Mathlibの微分をざっと見てきました．Mathlibにはこれまでに説明しなかった多くの情報が含まれています．例えば，1次元の設定での片側微分を使いたいとしましょう．これについてMathlibにはより一般的な文脈のものがあります; HasFDerivWithinAt や，さらに一般的な HasFDerivAtFilter を参照してください．