まとめ

積分の章では，MeasurableSpace，Measure，MeasurableSet，Integrable，∫ 記法，∀ᵐ 記法を読むことが第一歩です． 実数値積分だけを見ている場合でも，Mathlib の内部では Bochner 積分と測度論の一般的な枠組みが使われます．

したがって，積分の証明では，可測性，可積分性，完備性，σ有限性などの仮定がどこで必要になるかを #check で確認しながら進めるのが重要です．

形式化の tips

積分の形式化では，計算そのものよりも仮定の整理が難しいことが多いです．

1. 可測集合かどうかは MeasurableSet．
2. 関数の可測性は Measurable や AEStronglyMeasurable．
3. 積分可能性は Integrable．
4. ほとんど至る所は ∀ᵐ x ∂μ, ...．
5. 区間積分では IntervalIntegrable f volume a b．
6. 直積測度や Fubini では SigmaFinite または SFinite 仮定を確認する．