13. Integrasi dan Teori Ukuran

13.1. Integrasi Elementer

Mula-mula kita berfokus pada integrasi fungsi pada interval hingga di ℝ. Kita dapat mengintegralkan fungsi-fungsi elementer.

open MeasureTheory intervalIntegral

open Interval
-- ini memperkenalkan notasi `[[a, b]]` untuk ruas dari `min a b` hingga `max a b`

example (a b : ℝ) : (∫ x in a..b, x) = (b ^ 2 - a ^ 2) / 2 :=
  integral_id

example {a b : ℝ} (h : (0 : ℝ) ∉ [[a, b]]) : (∫ x in a..b, 1 / x) = Real.log (b / a) :=
  integral_one_div h

Teorema dasar kalkulus menghubungkan integrasi dengan diferensiasi. Di bawah ini kita berikan pernyataan yang disederhanakan dari kedua bagian teorema tersebut. Bagian pertama mengatakan bahwa integrasi memberikan invers bagi diferensiasi, sedangkan bagian kedua menentukan cara menghitung integral turunan. (Kedua bagian ini sangat berkaitan erat, tetapi versi optimalnya, yang tidak ditampilkan di sini, tidak ekuivalen.)

example (f : ℝ → ℝ) (hf : Continuous f) (a b : ℝ) : deriv (fun u ↦ ∫ x in a..u, f x) b = f b :=
  (integral_hasStrictDerivAt_right (hf.intervalIntegrable _ _) (hf.stronglyMeasurableAtFilter _ _)
        hf.continuousAt).hasDerivAt.deriv

example {f : ℝ → ℝ} {a b : ℝ} {f' : ℝ → ℝ} (h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x)
    (h' : IntervalIntegrable f' volume a b) : (∫ y in a..b, f' y) = f b - f a :=
  integral_eq_sub_of_hasDerivAt h h'

Konvolusi juga didefinisikan di Mathlib dan sifat-sifat dasarnya telah dibuktikan.

open Convolution

example (f : ℝ → ℝ) (g : ℝ → ℝ) : f ⋆ g = fun x ↦ ∫ t, f t * g (x - t) :=
  rfl

13.2. Teori Ukuran

Konteks umum untuk integrasi di Mathlib adalah teori ukuran. Bahkan integral elementer pada bagian sebelumnya sebenarnya merupakan integral Bochner. Integrasi Bochner adalah perumuman integrasi Lebesgue yang ruang sasarannya dapat berupa sembarang ruang Banach, tidak harus berdimensi hingga.

Komponen pertama dalam pengembangan teori ukuran adalah gagasan aljabar-\(\sigma\) atas himpunan-himpunan, yang anggotanya disebut himpunan terukur. Kelas tipe MeasurableSpace digunakan untuk melengkapi suatu tipe dengan struktur semacam ini. Himpunan empty dan univ bersifat terukur, komplemen himpunan terukur bersifat terukur, dan gabungan atau irisan terhitung dari himpunan-himpunan terukur juga bersifat terukur. Perhatikan bahwa aksioma-aksioma ini berlebihan; jika Anda menjalankan #print MeasurableSpace, Anda akan melihat aksioma yang digunakan Mathlib. Seperti diperlihatkan contoh-contoh di bawah, asumsi keterhitungan dapat dinyatakan menggunakan kelas tipe Encodable.

variable {α : Type*} [MeasurableSpace α]

example : MeasurableSet (∅ : Set α) :=
  MeasurableSet.empty

example : MeasurableSet (univ : Set α) :=
  MeasurableSet.univ

example {s : Set α} (hs : MeasurableSet s) : MeasurableSet (sᶜ) :=
  hs.compl

example : Encodable ℕ := by infer_instance

example (n : ℕ) : Encodable (Fin n) := by infer_instance

variable {ι : Type*} [Encodable ι]

example {f : ι → Set α} (h : ∀ b, MeasurableSet (f b)) : MeasurableSet (⋃ b, f b) :=
  MeasurableSet.iUnion h

example {f : ι → Set α} (h : ∀ b, MeasurableSet (f b)) : MeasurableSet (⋂ b, f b) :=
  MeasurableSet.iInter h

Setelah suatu tipe memiliki struktur terukur, kita dapat mengukurnya. Di atas kertas, ukuran pada himpunan (atau tipe) yang dilengkapi aljabar-\(\sigma\) adalah fungsi dari himpunan-himpunan terukur ke bilangan real nonnegatif diperluas. Fungsi tersebut bersifat aditif pada gabungan terhitung yang saling lepas. Di Mathlib, kita tidak ingin harus selalu membawa asumsi keterukuran setiap kali menuliskan penerapan ukuran pada suatu himpunan. Karena itu, ukuran diperluas ke sembarang himpunan s sebagai infimum ukuran himpunan-himpunan terukur yang memuat s. Tentu saja, banyak lema masih memerlukan asumsi keterukuran, meskipun tidak semuanya.

open MeasureTheory Function
variable {μ : Measure α}

example (s : Set α) : μ s = ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), μ t :=
  measure_eq_iInf s

example (s : ι → Set α) : μ (⋃ i, s i) ≤ ∑' i, μ (s i) :=
  measure_iUnion_le s

example {f : ℕ → Set α} (hmeas : ∀ i, MeasurableSet (f i)) (hdis : Pairwise (Disjoint on f)) :
    μ (⋃ i, f i) = ∑' i, μ (f i) :=
  μ.m_iUnion hmeas hdis

Setelah suatu tipe dilengkapi ukuran, kita mengatakan bahwa sifat P berlaku hampir di mana-mana jika himpunan elemen tempat sifat tersebut gagal memiliki ukuran 0. Kumpulan sifat yang berlaku hampir di mana-mana membentuk sebuah filter, tetapi Mathlib memperkenalkan notasi khusus untuk menyatakan bahwa suatu sifat berlaku hampir di mana-mana.

example {P : α → Prop} : (∀ᵐ x ∂μ, P x) ↔ ∀ᶠ x in ae μ, P x :=
  Iff.rfl

13.3. Integrasi

Setelah memiliki ruang terukur dan ukuran, kini kita dapat membahas integral. Seperti dijelaskan di atas, Mathlib menggunakan gagasan integrasi yang sangat umum sehingga sembarang ruang Banach dapat menjadi ruang sasaran. Seperti biasa, kita tidak ingin notasi harus selalu membawa asumsi. Karena itu, kita mendefinisikan integrasi sedemikian rupa sehingga integral bernilai nol jika fungsi yang bersangkutan tidak terintegralkan. Sebagian besar lema mengenai integral memiliki asumsi keterintegralan.

section
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : α → E}

example {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) :
    ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ :=
  integral_add hf hg

Sebagai contoh interaksi rumit di antara berbagai konvensi kita, mari kita lihat cara mengintegralkan fungsi konstan. Ingatlah bahwa ukuran μ bernilai dalam ℝ≥0∞, yaitu tipe bilangan real nonnegatif diperluas. Terdapat fungsi ENNReal.toReal : ℝ≥0∞ → ℝ yang memetakan ⊤, titik di takhingga, ke nol. Untuk sembarang s : Set α, jika μ s = ⊤, maka fungsi konstan taknol tidak terintegralkan pada s. Dalam hal itu, integralnya sama dengan nol menurut definisi, demikian pula (μ s).toReal. Jadi, dalam semua kasus kita memperoleh lema berikut.

example {s : Set α} (c : E) : ∫ _ in s, c ∂μ = (μ s).toReal • c :=
  setIntegral_const c

Sekarang kita jelaskan secara singkat cara mengakses teorema-teorema terpenting dalam teori integrasi, dimulai dengan teorema konvergensi terdominasi. Terdapat beberapa versi di Mathlib, dan di sini kita hanya menampilkan versi paling dasar.

open Filter

example {F : ℕ → α → E} {f : α → E} (bound : α → ℝ) (hmeas : ∀ n, AEStronglyMeasurable (F n) μ)
    (hint : Integrable bound μ) (hbound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a)
    (hlim : ∀ᵐ a ∂μ, Tendsto (fun n : ℕ ↦ F n a) atTop (𝓝 (f a))) :
    Tendsto (fun n ↦ ∫ a, F n a ∂μ) atTop (𝓝 (∫ a, f a ∂μ)) :=
  tendsto_integral_of_dominated_convergence bound hmeas hint hbound hlim

Selanjutnya, kita memiliki teorema Fubini untuk integral pada tipe produk.

example {α : Type*} [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ] {β : Type*}
    [MeasurableSpace β] {ν : Measure β} [SigmaFinite ν] (f : α × β → E)
    (hf : Integrable f (μ.prod ν)) : ∫ z, f z ∂ μ.prod ν = ∫ x, ∫ y, f (x, y) ∂ν ∂μ :=
  integral_prod f hf

Terdapat versi konvolusi yang sangat umum dan berlaku bagi sembarang bentuk bilinear kontinu.

open Convolution

variable {𝕜 : Type*} {G : Type*} {E : Type*} {E' : Type*} {F : Type*} [NormedAddCommGroup E]
  [NormedAddCommGroup E'] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E]
  [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedSpace ℝ F] [CompleteSpace F]
  [Sub G]

example (f : G → E) (g : G → E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : Measure G) :
    f ⋆[L, μ] g = fun x ↦ ∫ t, L (f t) (g (x - t)) ∂μ :=
  rfl

Terakhir, Mathlib memiliki versi yang sangat umum dari rumus perubahan variabel. Dalam pernyataan di bawah, BorelSpace E berarti bahwa aljabar-\(\sigma\) pada E dibangkitkan oleh himpunan-himpunan terbuka di E, sedangkan IsAddHaarMeasure μ berarti bahwa ukuran μ invarian-kiri, memberikan massa hingga pada himpunan kompak, dan memberikan massa positif pada himpunan terbuka.

example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {F : Type*}
    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {s : Set E} {f : E → E}
    {f' : E → E →L[ℝ] E} (hs : MeasurableSet s)
    (hf : ∀ x : E, x ∈ s → HasFDerivWithinAt f (f' x) s x) (h_inj : InjOn f s) (g : E → F) :
    ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ :=
  integral_image_eq_integral_abs_det_fderiv_smul μ hs hf h_inj g