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

타입에 측도가 연관되고 나면, 성질이 실패하는 원소들의 집합의 측도가 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∞에서 값을 취한다는 점을 상기하십시오. 무한대 점인 ⊤를 0으로 보내는 함수 ENNReal.toReal : ℝ≥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