12. Kalkulus Diferensial

Sekarang kita membahas formalisasi gagasan-gagasan dari analisis, dimulai dengan diferensiasi dalam bab ini, lalu beralih ke integrasi dan teori ukuran dalam bab berikutnya. Dalam Bab 12.1, kita tetap berada dalam tatanan fungsi dari bilangan real ke bilangan real, yang sudah akrab dari setiap kelas pengantar kalkulus. Kemudian, dalam Bab 12.2, kita membahas gagasan turunan dalam tatanan yang jauh lebih luas.

12.1. Kalkulus Diferensial Elementer

Misalkan f adalah fungsi dari bilangan real ke bilangan real. Ada perbedaan antara membahas turunan f pada satu titik dan membahas fungsi turunannya. Di Mathlib, gagasan pertama direpresentasikan sebagai berikut.

open Real

/-- Fungsi sin memiliki turunan 1 pada 0. -/
example : HasDerivAt sin 1 0 := by simpa using hasDerivAt_sin 0

Kita juga dapat menyatakan bahwa f terdiferensialkan pada suatu titik tanpa menentukan turunannya di sana dengan menulis DifferentiableAt ℝ. Kita menentukan ℝ secara eksplisit karena, dalam konteks yang sedikit lebih umum ketika membahas fungsi dari ℂ ke ℂ, kita ingin dapat membedakan sifat terdiferensialkan dalam pengertian real dari sifat terdiferensialkan dalam pengertian turunan kompleks.

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

Tidak praktis jika kita harus memberikan bukti keterdiferensialan setiap kali ingin merujuk pada suatu turunan. Karena itu, Mathlib menyediakan fungsi deriv f : ℝ → ℝ yang didefinisikan bagi setiap fungsi f : ℝ → ℝ, tetapi ditetapkan bernilai 0 pada setiap titik tempat f tidak terdiferensialkan.

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

Tentu saja, banyak lema tentang deriv memang memerlukan asumsi keterdiferensialan. Sebagai contoh, pikirkan sebuah contoh tandingan bagi lema berikut jika asumsi keterdiferensialannya dihapus.

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

Namun, menariknya, ada pernyataan yang dapat menghindari asumsi keterdiferensialan dengan memanfaatkan fakta bahwa nilai deriv secara bawaan adalah nol ketika fungsi tidak terdiferensialkan. Karena itu, untuk memahami pernyataan berikut, kita perlu mengetahui definisi tepat deriv.

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

Kita bahkan dapat menyatakan teorema Rolle tanpa asumsi keterdiferensialan apa pun, yang terasa lebih ganjil lagi.

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

Tentu saja, trik ini tidak berlaku bagi teorema nilai rata-rata umum.

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 dapat menghitung beberapa turunan sederhana secara otomatis menggunakan taktik simp.

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

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

12.2. Kalkulus Diferensial pada Ruang Bernorma

12.2.1. Ruang bernorma

Diferensiasi dapat diperumum melampaui ℝ dengan menggunakan gagasan ruang vektor bernorma, yang mencakup arah sekaligus jarak. Kita mulai dengan gagasan grup bernorma, yaitu grup komutatif aditif yang dilengkapi fungsi norma bernilai real dan memenuhi syarat-syarat berikut.

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

Setiap ruang bernorma adalah ruang metrik dengan fungsi jarak \(d(x, y) = \| x - y \|\), sehingga ruang tersebut juga merupakan ruang topologis. Lean dan Mathlib mengetahui fakta ini.

example : MetricSpace E := by infer_instance

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

Agar dapat menggunakan gagasan norma bersama konsep-konsep aljabar linear, kita menambahkan asumsi NormedSpace ℝ E di samping NormedAddGroup E. Asumsi ini menetapkan bahwa E adalah ruang vektor atas ℝ dan bahwa perkalian skalar memenuhi syarat berikut.

variable [NormedSpace ℝ E]

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

Ruang bernorma yang lengkap disebut ruang Banach. Setiap ruang vektor berdimensi hingga bersifat lengkap.

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

Pada semua contoh sebelumnya, kita menggunakan bilangan real sebagai medan dasar. Secara lebih umum, kalkulus dapat dibahas pada ruang vektor atas sembarang medan bernorma nontrivial. Medan semacam ini dilengkapi norma bernilai real yang bersifat multiplikatif dan memiliki sifat bahwa tidak semua elemennya bernorma nol atau satu (secara ekuivalen, terdapat suatu elemen yang normanya lebih besar dari satu).

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

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

Ruang vektor berdimensi hingga atas medan bernorma nontrivial bersifat lengkap asalkan medannya sendiri lengkap.

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

12.2.2. Pemetaan linear kontinu

Sekarang kita beralih ke morfisme dalam kategori ruang bernorma, yaitu pemetaan linear kontinu. Di Mathlib, tipe pemetaan kontinu yang linear atas 𝕜 dari ruang bernorma E ke F ditulis E →L[𝕜] F. Pemetaan tersebut diimplementasikan sebagai pemetaan terbundel. Artinya, sebuah elemen bertipe ini merupakan struktur yang memuat fungsi itu sendiri beserta sifat linear dan kontinunya. Lean akan menyisipkan koersi agar pemetaan linear kontinu dapat diperlakukan sebagai fungsi.

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

Pemetaan linear kontinu memiliki norma operator yang dicirikan oleh sifat-sifat berikut.

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

Terdapat pula gagasan isomorfisme linear kontinu terbundel. Tipe isomorfisme semacam itu adalah E ≃L[𝕜] F.

Sebagai latihan yang menantang, Anda dapat membuktikan teorema Banach--Steinhaus, yang juga dikenal sebagai Prinsip Keterbatasan Seragam. Prinsip tersebut menyatakan bahwa jika suatu keluarga pemetaan linear kontinu dari ruang Banach ke ruang bernorma terbatas secara titik demi titik, maka norma-norma pemetaan linear itu terbatas secara seragam. Bahan utamanya adalah teorema Baire nonempty_interior_of_iUnion_of_closed. (Anda telah membuktikan suatu versi teorema ini dalam bab topologi.) Bahan-bahan kecilnya mencakup ContinuousLinearMap.opNorm_le_of_shell, interior_subset, interior_iInter_subset, dan 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
  -- barisan himpunan bagian berisi `x : E` dengan norma `‖g i x‖` yang dibatasi oleh `n`
  let e : ℕ → Set E := fun n ↦ ⋂ i : ι, { x : E | ‖g i x‖ ≤ n }
  -- setiap himpunan ini tertutup
  have hc : ∀ n : ℕ, IsClosed (e n)
  sorry
  -- gabungannya adalah seluruh ruang; di sinilah kita menggunakan `h`
  have hU : (⋃ n : ℕ, e n) = univ
  sorry
  /- terapkan teorema kategori Baire untuk menyimpulkan bahwa, bagi suatu `m : ℕ`,
       interior `e m` memuat suatu `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
  -- tunjukkan bahwa norma setiap elemen bola dibatasi oleh `m` setelah diterapkan sembarang `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. Perbandingan asimtotik

Mendefinisikan keterdiferensialan juga memerlukan perbandingan asimtotik. Mathlib memiliki pustaka luas yang mencakup relasi O besar dan o kecil; definisi keduanya diperlihatkan di bawah ini. Perintah open Asymptotics memungkinkan kita menggunakan notasi yang bersesuaian. Di sini kita hanya akan menggunakan o kecil untuk mendefinisikan keterdiferensialan.

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. Keterdiferensialan

Sekarang kita siap membahas fungsi terdiferensialkan di antara ruang-ruang bernorma. Sejalan dengan kalkulus elementer satu dimensi, Mathlib mendefinisikan predikat HasFDerivAt dan fungsi fderiv. Di sini huruf "f" merupakan singkatan dari 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

Kita juga memiliki turunan berulang yang nilainya bertipe pemetaan multilinear E [×n]→L[𝕜] F, serta fungsi yang terdiferensialkan secara kontinu. Tipe ℕ∞ adalah ℕ dengan satu elemen tambahan ∞ yang lebih besar daripada setiap bilangan asli. Jadi, fungsi \(\mathcal{C}^\infty\) adalah fungsi f yang memenuhi ContDiff 𝕜 ⊤ 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

Parameter keterdiferensialan dalam ContDiff juga dapat bernilai ω : WithTop ℕ∞ untuk menyatakan fungsi analitik.

Terdapat gagasan keterdiferensialan yang lebih ketat, bernama HasStrictFDerivAt, yang digunakan dalam pernyataan teorema fungsi invers dan teorema fungsi implisit; keduanya tersedia di Mathlib. Di atas ℝ atau ℂ, fungsi yang terdiferensialkan secara kontinu juga terdiferensialkan secara ketat.

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'

Teorema invers lokal dinyatakan menggunakan suatu operasi yang menghasilkan fungsi invers dari sebuah fungsi, dengan asumsi bahwa fungsi tersebut terdiferensialkan secara ketat pada titik a dan turunannya merupakan suatu isomorfisme.

Contoh pertama di bawah ini memperoleh invers lokal tersebut. Contoh-contoh berikutnya menyatakan bahwa fungsi itu memang merupakan invers lokal dari kiri dan dari kanan, serta terdiferensialkan secara ketat.

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

Bagian ini hanyalah tinjauan singkat atas kalkulus diferensial di Mathlib. Pustaka tersebut memuat banyak variasi yang belum kita bahas. Sebagai contoh, Anda mungkin ingin menggunakan turunan satu sisi dalam konteks satu dimensi. Sarana untuk melakukannya tersedia di Mathlib dalam konteks yang lebih umum; lihat HasFDerivWithinAt atau HasFDerivAtFilter yang bahkan lebih umum.