Instead of creating a new file, can you put your additions in the already existing file on the Riesz content? Otherwise, this makes the PR very hard to review (I don't know what is new material and what was already there).

OK sorry, I wasn't sure whether I should change the existing file because I changed the whole setting from ℝ≥0 to ℝ. Now I removed the new file and replaced the old file with mine.

Oops, my bad, I hadn't noticed that you had switched from NNReal to Real. Can you explain the reason for this choice? It seems to me that most things down the road should be easier using NNReal-valued functions (in particular because the topology on spaces of measures is defined using such functions), so I'd rather use them unless they create a difficulty somewhere.

I changed from NNReal to Real because I have in mind the application of the RMK theorem to prove the spectral decomposition. There one would need even complex valued functionals, complex-valued measures, and so on, but I thought it was a good start to use linear structures rather than NNReal. What do you think?

For complex measures, one should definitely use complex-valued functions. For real measures, real-valued functions. And for measures in the usual sense, which are nonnegative, then NNReal-valued functions looks like the most natural choice. We have already code duplication between measures and vector-valued measures, but this seems unavoidable.

so do you mean that I should make a new file, say "RealRieszMarkovKakutani.lean" and keep the NNReal version as is?

I mean for now we should just use NNReal and do everything with them. Once we have Riesz-Markov-Kakutani for measures, we may start thinking on what we want to do with real measures or complex measures (or vector-valued measures), but it wouldn't make sense to do it before we complete it for usual measures, because when doing it we will learn a lot.

Ok, then I will bring back NNReal and the Real version as a separate file

Ok, then I will bring back NNReal and the Real version as a separate file

For now, I'd say we shouldn't even have the Real version at all, and only do the NNReal one.

I see, I will do that.

Oops. I should have remembered to remove the cases IsEmpty part of the argument after the other parts were updated. Now corrected. Sorry for overly taking advantage of the reviewer here!

bors r+
Many many thanks for getting this into mathlib, both to @yoh-tanimoto and @oliver-butterley!

Build failed:

• Build

The bors build fails since Order.Interval.Set.Basic was split in #23556. I'll merge in master and then update the imports in Union.lean.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style