Chapter 05: 積分

Mathlib における基本的な測度と積分を扱います．

• Mathematics in Lean, 13. Integration and Measure Theory: https://leanprover-community.github.io/mathematics_in_lean/C13_Integration_and_Measure_Theory.html

区間積分，測度論，Bochner 積分，優収束定理，Fubini の定理などが概観されています．

Mathlib の積分はかなり一般的です． 実数値関数だけでなく，Banach 空間値の Bochner 積分を基本としており，測度は Measure α，値は拡張非負実数 ℝ≥0∞ を使います．

import Mathlib

namespace PracticeChapter05

noncomputable section

open Set Filter MeasureTheory
open scoped BigOperators ENNReal Topology Interval