Papers With

← All papers
cs.LO

Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality

Floris van Doorn, Heather Macbeth

cs.LO Sep 2, 2024 · v1
formalization mathlib analysis
Read PDF arXiv abstract
TL;DR
Formalizes iterated integrals and the Gagliardo-Nirenberg-Sobolev inequality in Lean's mathlib.
Abstract
We introduce an abstraction which allows arguments involving iterated integrals to be formalized conveniently in type-theory-based proof assistants. We call this the marginal construction, connected to marginal distributions in probability theory. It handles permutations to the order of integration (Tonelli's theorem in several variables) and arguments involving induction over dimension. We implement this in Lean, with the most difficult application being the Gagliardo-Nirenberg-Sobolev inequality, a foundational result in the theory of elliptic partial differential equations that has not previously been formalized.
Problem

Arguments involving iterated integrals are difficult to formalize in type-theory-based proof assistants due to permutations of integration order (Tonelli's theorem in several variables) and induction over dimension.

Approach

The authors introduce the marginal construction, an abstraction connected to marginal distributions in probability theory, that handles permutations of integration order and dimension induction. They implement this in Lean and apply it to formalize the Gagliardo-Nirenberg-Sobolev inequality, a foundational result in elliptic PDE theory.

Results

The Gagliardo-Nirenberg-Sobolev inequality is formalized for the first time in any proof assistant. The marginal construction provides a reusable abstraction for iterated integration arguments in Lean.