収束定理と Fubini の定理

測度論の大きな定理も Mathlib に登録されています． 最初は全文を展開するより，定理名と型を確認して使うのが現実的です．

#check tendsto_integral_of_dominated_convergence
#check integral_prod
#check integral_image_eq_integral_abs_det_fderiv_smul

section Fubini

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

example (f : α × β → E) (hf : Integrable f (μ.prod ν)) :
    ∫ z, f z ∂ μ.prod ν = ∫ x, ∫ y, f (x, y) ∂ν ∂μ := by
  exact integral_prod f hf

end Fubini

演習問題

1. Fubini の定理の statement を #check で読み，どこに SigmaFinite 仮定が現れるか確認してください．

   #check integral_prod
   

2. 優収束定理の statement を読み，どの仮定が「支配関数」に対応するか確認してください．

   #check tendsto_integral_of_dominated_convergence