Riemann integral

Stream: Is there code for X?

[Xavier Roblot]

The Riemann integral can defined using Mathlib.Analysis.BoxIntegral.Basic and shown to exist for continuous functions using docs#BoxIntegral.integrable_of_continuousOn. However, there doesn't seem to be any result relating it to the Bochner integral since all the results in Mathlib.Analysis.BoxIntegral.Integrability have l.bRiemann = false as hypothesis. Is that correct?

[Xavier Roblot]

I am interested in proving that the limit of the Riemann sums for some nonnegative continuous function is equal to the integral of the function.

[Xavier Roblot]

Well, turns out it is easy to deduce the result from existing results for continuous functions, see #10144