Coq中的Lebesgue归纳法与Tonelli定理
Lebesgue Induction and Tonelli's Theorem in Coq
摘要：
勒贝格积分是一种著名的数学工具，例如用于概率论、实分析和数值数学。因此，它在证明助手中的形式化被设计成适合不同的目标和项目。一旦勒贝格积分的正式定义和第一引理证明，方便的问题的形式化自然出现。为了检验它，一个有用的扩展是托内利定理，指出一个非负的两个变量的可测函数的（二重）积分可以通过迭代积分计算，并允许切换积分的顺序。因此，我们需要定义和证明乘积空间上的结果，希望它们可以很容易地从单个空间上的现有结果导出。本文描述了乘积$σ$ -代数的形式定义和证明，乘积测度及其唯一性，迭代积分的构造，直到Tonelli定理。我们还为{ \nonnegative }可测函数宣传归纳类型提供的\emph{Lebesgue induction principle}。
英文摘要：
Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus its formalization in a proof assistant is to be designed to fit different goals and projects. Once Lebesgue integral is formally defined and the first lemmas are proved, the question of the convenience of the formalization naturally arises. To check it, a useful extension is the Tonelli theorem, stating that the (double) integral of a nonnegative measurable function of two variables can be computed by iterated integrals, and allowing to switch the order of integration. Therefore, we need to define and prove results on product spaces, hoping that they can easily derive from the existing ones on a single space. This article describes the formal definition and proof in Coq of product $σ$-algebras, product measures and their uniqueness, the construction of iterated integrals, up to the Tonelli theorem. We also advertise the \emph{Lebesgue induction principle} provided by an inductive type for {\nonnegative} measurable functions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
