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 theorem)를 증명할 수 있습니다. 이 원리는 바나흐 공간에서 노름 공간으로의 연속 선형 사상들의 족이 점별로 유계이면, 이 선형 사상들의 노름이 균등하게 유계라는 것을 말합니다. 핵심 재료는 베르 정리(Baire’s theorem)인 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에는 빅 오(big O)와 리틀 오(little o) 관계를 다루는 방대한 라이브러리가 있으며, 그 정의는 아래에 나와 있습니다. 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

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의 미분법을 간단히 둘러보았습니다. 라이브러리에는 여기서 다루지 않은 다양한 변형이 포함되어 있습니다. 예를 들어, 일차원 환경에서 한쪽 도함수를 사용하고 싶을 수도 있습니다. 이를 수행하는 방법은 Mathlib에 더 일반적인 맥락으로 마련되어 있으니, HasFDerivWithinAt이나 더욱 일반적인 HasFDerivAtFilter를 참고하십시오.