Commit 2025-04-06 07:44 9a330325

View on Github →

chore(RadonNikodym): move SignedMeasure lemmas to a new file (#23618) Also golf and add setIntegral_rnDeriv_smul'.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

Modified Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean

Modified Mathlib/MeasureTheory/Measure/Decomposition/Hahn.lean

Modified Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean

deleted theorem MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq

deleted theorem MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq

added theorem MeasureTheory.setIntegral_rnDeriv_smul'

deleted theorem MeasureTheory.withDensityᵥ_rnDeriv_smul

Created Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean

added theorem MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq

added theorem MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq

added theorem MeasureTheory.withDensityᵥ_rnDeriv_smul