Dylan Crooks (Jan 29 2025 at 21:57): Dylan Crooks (Jan 29 2025 at 21:57):Hey, I'm a beginner to both Isabelle and mathematics in general. I didn't find any formulation of the Riemann integral in the AFP, notably, Laurence Paulson avoided them when proved Young's Inequality.
I'm wondering why aren't Riemann integrals formalized?
In particular, I wanted to try to formalize and prove basic properties of the Choquet integral, which uses the Riemann integral in its definition (according to wikipedia). I assume I could use Lebesgue integrals instead, but then I would have to define it to exclude functions that aren't riemann integrable.
Christian Pardillo Laursen (Jan 30 2025 at 22:03):The reason for this, I imagine, is practicality. HOL-Analysis defines the non-negative lebesgue integral, but the full lebesgue integral is defined in terms of the Bochner integral since they are equal on all lebesgue-integrable functions. Similarly, the Riemann integral is equal to the Lebesgue integral on all riemann-integrable functions, and so for the standard library it didn't make sense to have both available when one is simply more general.
So indeed, if you can use the Lebesgue integral do so, since all lebesgue integrable functions are riemann integrable.
Christian Pardillo Laursen (Jan 30 2025 at 22:13):Looking at the wikipedia page for the choquet integral I see no reason why you wouldn't be able to formalise it with the lebesgue integral over the lebesgue measure.
Yosuke Ito (Feb 01 2025 at 02:29):In my understanding, Isabelle/HOL formalizes the Henstock–Kurzweil integral, which is a generalization of the Riemann integral.
Last updated: Feb 01 2025 at 20:19 UTC