论文标题
Bochner积分的COQ形式化
A Coq Formalization of the Bochner integral
论文作者
论文摘要
Bochner积分是Lebesgue积分的概括，用于在Banach空间中占据其价值。因此，由于我们不能依靠实数的属性，因此其数学定义及其在COQ证明助手中的形式化都更具挑战性。我们的贡献包括简单函数的原始形式化，由依赖类型定义的Bochner集成性以及在轻度假设下可测量功能的整合性的构建（弱可分离性）。然后，我们定义了Bochner积分并证明了几个定理，包括主导的收敛性和与非负功能的Lebesgue积分现有形式化的等效性。
The Bochner integral is a generalization of the Lebesgue integral, for functions taking their values in a Banach space. Therefore, both its mathematical definition and its formalization in the Coq proof assistant are more challenging as we cannot rely on the properties of real numbers. Our contributions include an original formalization of simple functions, Bochner integrability defined by a dependent type, and the construction of the proof of the integrability of measurable functions under mild hypotheses (weak separability). Then, we define the Bochner integral and prove several theorems, including dominated convergence and the equivalence with an existing formalization of Lebesgue integral for nonnegative functions.
