Bochner 積分

Mathlib の標準的な積分 ∫ x, f x ∂μ は Bochner 積分です． 値域は実数だけでなく，完備なノルム空間に一般化されています． 多くの定理では Integrable f μ という仮定を使います．

#check Integrable
#check integral_add
#check setIntegral_const

section BochnerIntegral

variable {α : Type*} [MeasurableSpace α]
variable {μ : Measure α}
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]

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

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

end BochnerIntegral

定数関数の積分では，測度値 μ s : ℝ≥0∞ を実数に戻すために (μ s).toReal が現れます． μ s = ∞ の場合には，非零定数関数は可積分でなく，積分は定義上 0 になるという規約とも整合しています．

演習問題

Bochner 積分の加法性を使ってください．

example {α E : Type*} [MeasurableSpace α]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {μ : Measure α} {f g : α → E}
    (hf : Integrable f μ) (hg : Integrable g μ) :
    ∫ x, f x + g x ∂μ = ∫ x, f x ∂μ + ∫ x, g x ∂μ := by
  -- ヒント: `exact integral_add hf hg`
  sorry