Localic Caratheodory Extensions

This repository contains a formalization of localic measure theory – specifically, the Carathéodory extension of measure in the setting of locales. It builds on the foundational work in locale theory (nuclei, sublocales, and their intersections) and formalizes the main result from Olivier Leroy’s 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

The key achievement of this project is the formal proof that the Carathéodory extension of measure on locales is both strictly additive and μ-reducible.

Useful links:

• Zulip chat for Lean for coordination
• Blueprint
• Blueprint as pdf
• Main Dependency graph
• Doc pages for this repository