Commit 2025-02-09 23:04 58238a71

View on Github →

feat: Carathéodory's Extension Theorem (#21353) Show that an AddContent on a SetSemiring gives rise to an inducedOuterMeasure. All sets in the measurable structure generated by the SetSemiring are Carathéodory measurable.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/AddContent.lean

added def MeasureTheory.AddContent.IsSigmaSubadditive

added theorem MeasureTheory.addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive

Created Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean

added theorem MeasureTheory.AddContent.inducedOuterMeasure_eq

added theorem MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure

added theorem MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem

added theorem MeasureTheory.AddContent.isCaratheodory_ofFunction_of_mem

added theorem MeasureTheory.AddContent.measureCaratheodory_eq

added theorem MeasureTheory.AddContent.measureCaratheodory_eq_inducedOuterMeasure

added theorem MeasureTheory.AddContent.measure_eq

added theorem MeasureTheory.AddContent.ofFunction_eq