Commit 2026-08-24 08:10 af5b7e58

View on Github →

refactor(MeasureTheory/Integral): split long file SetToL1.lean (#43021) Split this file, currently 1500 - ɛ lines, into 5 pieces as follows:

  • Mathlib.MeasureTheory.Integral.SetToL1.SimpleFunc (338 lines): extension from sets to L¹ simple functions
  • Mathlib.MeasureTheory.Integral.SetToL1.L1 (274 lines): extension to continuous linear maps on L¹
  • Mathlib.MeasureTheory.Integral.SetToL1.Function (355 lines): extension to integrable functions
  • Mathlib.MeasureTheory.Integral.SetToL1.ChangeMeasure (287 lines): compatibility with changes of measure
  • Mathlib.MeasureTheory.Integral.SetToL1.DominatedConvergence (343 lines): convergence and measurability results for the extension

Estimated changes

deleted theorem MeasureTheory.setToFun_eq
deleted theorem measurableSet_integrable