12. 미분학

이제 해석학의 개념을 형식화하는 문제를 살펴보겠습니다. 이 장에서는 미분부터 시작하고, 다음 장에서는 적분과 측도론을 다룹니다. 제 12.1 절에서는 입문 미적분학 수업에서 익숙하게 접하는 설정, 즉 실수에서 실수로 가는 함수를 계속 다룹니다. 이어서 제 12.2 절에서는 훨씬 더 넓은 설정에서 도함수의 개념을 살펴봅니다.

12.1. 기초 미분학

f를 실수에서 실수로 가는 함수라고 합시다. 한 점에서 f의 도함수를 말하는 것과 도함수를 하나의 함수로서 말하는 것에는 차이가 있습니다. Mathlib에서 첫 번째 개념은 다음과 같이 나타냅니다.

open Real

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

DifferentiableAt ℝ을 쓰면 한 점에서의 도함수를 명시하지 않고도 f가 그 점에서 미분 가능하다는 것을 표현할 수도 있습니다. 조금 더 일반적인 문맥에서 ℂ에서 ℂ로 가는 함수를 다룰 때에는 실수의 의미에서 미분 가능한 것과 복소 도함수의 의미에서 미분 가능한 것을 구별할 수 있어야 하므로 ℝ을 명시적으로 지정합니다.

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

도함수를 언급할 때마다 미분 가능성의 증명을 제공해야 한다면 불편할 것입니다. 그래서 Mathlib은 모든 함수 f : ℝ → ℝ에 대해 정의되는 함수 deriv 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 := by
  exact?
  --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

12.2. 노름 공간에서의 미분법

12.2.1. 노름 공간

미분은 방향과 거리를 모두 담아내는 노름 벡터 공간이라는 개념을 이용하여 ℝ 너머로 일반화할 수 있습니다. 먼저 노름 군이라는 개념에서 시작합니다. 노름 군은 다음 조건을 만족하는 실숫값 노름 함수를 갖춘 덧셈 가환군입니다.

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

완비 노름 공간을 바나흐 공간이라고 합니다. 모든 유한 차원 벡터 공간은 완비입니다.

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

앞의 모든 예제에서는 실수를 기초체로 사용했습니다. 더 일반적으로는 임의의 자명하지 않은 노름체 위의 벡터 공간에서도 미적분을 의미 있게 다룰 수 있습니다. 이는 곱셈적인 실숫값 노름을 갖추고 있으며, 모든 원소의 노름이 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

12.2.2. 연속 선형 사상

이제 노름 공간 범주의 사상, 즉 연속 선형 사상으로 넘어갑니다. Mathlib에서 노름 공간 E와 F 사이의 𝕜-선형 연속 사상의 타입은 E →L[𝕜] F로 표기합니다. 이들은 묶인 사상으로 구현되어 있는데, 이는 이 타입의 원소가 함수 자체와 함께 선형성 및 연속성이라는 성질을 포함하는 구조체라는 뜻입니다. 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

묶인 연속 선형 동형사상이라는 개념도 있습니다. 이러한 동형사상의 타입은 E ≃L[𝕜] F입니다.

도전적인 연습 문제로, 균등 유계성 원리(Uniform Boundedness Principle)라고도 알려진 바나흐-슈타인하우스(Banach-Steinhaus) 정리를 증명해 볼 수 있습니다. 이 원리에 따르면, 바나흐 공간에서 노름 공간으로 가는 연속 선형 사상들의 족이 점별로 유계이면 이 선형 사상들의 노름은 균등하게 유계입니다. 핵심 재료는 베르(Baire) 정리 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 : ℕ`,
       the interior of `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

12.2.3. 점근적 비교

미분 가능성을 정의하려면 점근적 비교도 필요합니다. Mathlib에는 빅 O 관계와 리틀 o 관계를 다루는 방대한 라이브러리가 있으며, 그 정의는 아래와 같습니다. asymptotics 로케일을 열면 해당 표기법을 사용할 수 있습니다. 여기서는 미분 가능성을 정의하는 데 리틀 o만 사용하겠습니다.

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

12.2.4. 미분 가능성

이제 노름 공간 사이의 미분 가능한 함수를 다룰 준비가 되었습니다. 기초적인 1차원의 경우와 마찬가지로, 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₀ :=
  hasFDerivAt_iff_isLittleO

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

또한 다중선형 사상의 타입 E [×n]→L[𝕜] F에 값을 갖는 반복 도함수가 있으며, 연속 미분 가능 함수도 있습니다. ℕ∞ 타입은 ℕ에 모든 자연수보다 큰 원소 ∞를 추가한 것입니다. 따라서 \(\mathcal{C}^\infty\) 함수는 ContDiff 𝕜 ⊤ f를 만족하는 함수 f입니다.

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

example (n : ℕ∞) {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

ContDiff의 미분 가능성 매개변수는 해석 함수를 나타내기 위해 ω : WithTop ℕ∞ 값을 가질 수도 있습니다.

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 (zero_lt_one.trans_le hn).ne'

국소 역함수 정리는 함수 하나와 두 가지 가정, 즉 그 함수가 점 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 (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의 미분학을 간단히 둘러보았습니다. 라이브러리에는 여기서 다루지 않은 다양한 변형이 많이 있습니다. 예를 들어, 1차원 설정에서 한쪽 도함수를 사용하고 싶을 수도 있습니다. 이를 위한 수단은 Mathlib에서 더 일반적인 문맥으로 제공됩니다. HasFDerivWithinAt 또는 이보다 더 일반적인 HasFDerivAtFilter를 참고하십시오.