Stream: Beginner Questions

Topic: Riemann Integrals

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (Feb 02 2025 at 14:32):

Henstock–Kurzweil and Lebesgue/Bochner are both in HOL-Analysis and there are theorems that relate the two to one another as well.

view this post on Zulip Manuel Eberl (Feb 02 2025 at 14:34):

And yes, both are a generalisation of Riemann. I for one have never found myself in a situation where I needed Riemann. But it's probably not too hard to define using the formalisation of HK as an inspiration.

Last updated: Mar 09 2025 at 12:28 UTC