Measure Construction by Extension in Dependent Type Theory with Application to Integration

Reynald Affeldt, Cyril Cohen

We report on an original formalization of measure and integration theory in the Coq proof assistant. We build the Lebesgue measure following a standard construction that had not ye…