12. 積分と測度論

12.1. 初等的な積分

ここではまず， ℝ の有限区間上の関数の積分に焦点を当てます．Mathlibでは初等関数を積分できます．

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

12.2. 測度論

Mathlibにおける積分の一般的な文脈は測度論です．前節の初等積分でさえも，実際にはボホナー積分です．ボホナー積分はルベーグ積分の一般化で，対象の空間はバナッハ空間であれば何でもよく，必ずしも有限次元である必要はありません．

測度論の発展における最初の要素は 可測 （measurable）集合と呼ばれる集合の \(\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
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 が ほとんどいたるところ （almost everywhere）で保持されるとは，その特性が失敗する要素の集合が測度0であることを指します．ほとんどいたるところで保持される特性の集合はフィルタを形成しますが，Mathlibはある特性がほとんどいたるところで保持されることを言うための特別な記法を導入しています．

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

12.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 = ⊤ ならば，非零定数関数は s 上で積分できません．その場合，積分は定義から (μ s).toReal となり，0に等しくなります．したがって，すべての場合において次の補題が成り立ちます．

example {s : Set α} (c : E) : ∫ x 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