Riesz-Markov-Kakutani representation theorem

Stream: Is there code for X?

[Kalle Kytölä]

We are considering the Riesz-Markov-Kakutani representation theorem (probably following Rudin's Real and Complex Analysis) as a topic for a summer intern. Although the primary goal is to have a topic for a summer project and not necessarily directly contribute to mathlib (we can decide about that later), I think it is nicer to choose a topic that doesn't obviously duplicate work (especially by experts). So: is anyone working / planning to work on that now or during the summer?

One implementation choice that I will suggest is to treat nnreal-valued functions first (the "positive linear functional" part is then naturally baked in, and the measures are usual ennreal-valued measures) and only later extend to real-valued functions and signed measures. This is inspired by how docs#measure_theory.finite_measure.topological_space was done following Heather's suggestion (I realize that I have not yet PR'd the pairing with real-valued functions there, but I will, soon). Comments are of course welcome! And we'd keep asking questions here :smile:.

[Frédéric Dupuis]

That sounds like a great project, I for one would be very happy to see this in mathlib!