13. 적분과 측도론

13.1. 기초 적분

먼저 ℝ의 유한 구간에서 정의된 함수의 적분을 중점적으로 다룹니다. 초등 함수를 적분할 수 있습니다.

open MeasureTheory intervalIntegral

open Interval
-- this introduces the notation `[[a, b]]` for the segment from `min a b` to `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

미적분학의 기본 정리는 적분과 미분을 연결합니다. 아래에서는 이 정리를 구성하는 두 부분을 단순화한 명제를 제시합니다. 첫 번째 부분은 적분이 미분의 역연산이 된다는 것을 말하고, 두 번째 부분은 도함수의 적분을 계산하는 방법을 명시합니다. (이 두 부분은 매우 밀접하게 연관되어 있지만, 여기서 다루지 않는 각각의 최적 버전은 서로 동치가 아닙니다.)

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'

합성곱 또한 Mathlib에 정의되어 있으며 그 기본 성질들이 증명되어 있습니다.

open Convolution

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

13.2. 측도론

Mathlib에서 적분을 다루는 일반적인 문맥은 측도론입니다. 앞 절에서 다룬 기초적인 적분들도 실은 보흐너 적분입니다. 보흐너 적분은 르베그 적분을 일반화한 것으로, 대상 공간이 반드시 유한 차원일 필요 없이 임의의 바나흐 공간일 수 있습니다.

측도론을 전개하는 첫 번째 구성 요소는 집합들의 \(\sigma\)-대수라는 개념이며, 이 집합들을 가측 집합이라고 부릅니다. 타입 클래스 MeasurableSpace는 타입에 이러한 구조를 부여하는 역할을 합니다. 집합 empty와 univ는 가측이고, 가측 집합의 여집합은 가측이며, 가측 집합들의 가산 합집합이나 가산 교집합도 가측입니다. 이 공리들에는 중복이 있다는 점에 유의하십시오. #print MeasurableSpace를 실행하면 Mathlib이 사용하는 공리들을 확인할 수 있습니다. 아래 예제에서 볼 수 있듯이, 가산성 가정은 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

타입이 가측이 되면, 그 위에 측도를 정의할 수 있습니다. 수학 교재에서는 \(\sigma\)-대수가 주어진 집합(또는 타입) 위의 측도를, 가측 집합들에서 확장된 음이 아닌 실수로 가는 함수이면서 가산 개의 서로소 합집합에 대해 가법적인 함수로 정의합니다. Mathlib에서는 집합에 측도를 적용할 때마다 가측성 가정을 일일이 달고 다니고 싶지 않습니다. 그래서 측도를 임의의 집합 s로 확장하여, s를 포함하는 가측 집합들의 측도의 하한으로 정의합니다. 물론 많은 보조정리에는 여전히 가측성 가정이 필요하지만, 모든 보조정리가 그런 것은 아닙니다.

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

타입에 측도가 연관되면, 성질 P가 성립하지 않는 원소들의 집합의 측도가 0일 때 P가 거의 어디서나 성립한다고 말합니다. 거의 어디서나 성립하는 성질들의 모임은 필터를 이루지만, Mathlib은 어떤 성질이 거의 어디서나 성립한다는 것을 나타내기 위한 특별한 표기법을 도입합니다.

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

13.3. 적분

이제 가측 공간과 측도를 갖추었으므로 적분을 다룰 수 있습니다. 앞에서 설명했듯이, Mathlib은 임의의 바나흐 공간을 공역으로 허용하는 매우 일반적인 적분 개념을 사용합니다. 늘 그렇듯이 표기법에 가정이 따라다니는 것을 원하지 않으므로, 해당 함수가 적분 가능하지 않으면 적분값이 0이 되도록 적분을 정의합니다. 적분과 관련된 대부분의 보조정리에는 적분 가능성 가정이 붙어 있습니다.

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

여러 규약이 복잡하게 얽히는 예로, 상수 함수를 적분하는 방법을 살펴봅시다. 측도 μ는 확장된 음이 아닌 실수의 타입인 ℝ≥0∞에서 값을 가진다는 점을 떠올려 보십시오. ENNReal.toReal : ℝ≥0∞ → ℝ 함수가 있는데, 이 함수는 무한대의 점인 ⊤를 0으로 보냅니다. 임의의 s : Set α에 대해 μ s = ⊤이면, 0이 아닌 상수 함수는 s 위에서 적분 가능하지 않습니다. 이 경우 그 적분값은 정의에 의해 0이며, (μ s).toReal도 마찬가지입니다. 따라서 모든 경우에 다음 보조정리가 성립합니다.

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

이제 지배 수렴 정리부터 시작하여 적분론에서 가장 중요한 정리들을 사용하는 방법을 간략히 설명합니다. Mathlib에는 여러 버전이 있으며, 여기서는 가장 기본적인 버전만 소개합니다.

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

다음으로 곱 타입 위의 적분에 대한 푸비니 정리가 있습니다.

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

임의의 연속 쌍선형 형식에 적용되는 매우 일반적인 버전의 합성곱이 있습니다.

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

마지막으로, Mathlib에는 매우 일반적인 버전의 변수 변환 공식이 있습니다. 아래 명제에서 BorelSpace E는 E 위의 \(\sigma\)-대수가 E의 열린 집합들로 생성된다는 뜻이고, IsAddHaarMeasure μ는 측도 μ가 좌불변이며, 컴팩트 집합에 유한한 질량을 부여하고, 열린 집합에 양의 질량을 부여한다는 뜻입니다.

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