Formalization of caratheodory extension on Locales

Stream: general

[Christian K]

Hey everyone,

I’m excited to share our Lean formalization of the Paper Théorie de la mesure dans les lieux réguliers. ou : Les intersections cachées dans le paradoxe de Banach-Tarski
arXiv:1303.5631 by Olivier Leroy, which claims, that the caratheodory extension of a measure on locales is both strictly additive and μ-reducible.
We have formalized the required foundations in locale theory (namely: Nuclei (already in Mathlib) and Sublocales and their interactions). Additionally, we have formalized several properties of the caratheodory extension of a measure on locales (including strict additivity and μ-reducibility)
The project is still under development and need some cleaning up, but we are planning to upstream our results to mathlib (especially the basics of locale theory).
You are welcome to check out our repo on github

[Christian K]

What’s your opinion on defining sublocales in mathlib? We defined them as the Nuclei equipped with dual ordering. Do you think this is the best approach, or would another formulation be better?