Commit 2026-03-06 15:35 1202f7b7

View on Github →

feat: Radon-Nikodym derivative of a map is a conditional expectation (#35089) The Radon-Nikodym derivative of the pushforward of two measures is written as a conditional expectation. This will be useful to prove the data processing inequality for the Kullback-Leibler divergence (or more generally f-divergences).

Estimated changes

Modified Mathlib.lean

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

Created Mathlib/MeasureTheory/Function/ConditionalExpectation/LebesgueBochner.lean

added theorem MeasureTheory.toReal_condLExp

Created Mathlib/MeasureTheory/Function/ConditionalExpectation/RadonNikodym.lean

added theorem MeasureTheory.rnDeriv_map

added theorem MeasureTheory.rnDeriv_map_ae_eq_trim

added theorem MeasureTheory.rnDeriv_trim

added theorem MeasureTheory.toReal_rnDeriv_map

added theorem MeasureTheory.toReal_rnDeriv_map_ae_eq_trim

added theorem MeasureTheory.toReal_rnDeriv_trim

Modified Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean

added theorem MeasureTheory.condLExp_lt_top

added theorem MeasureTheory.condLExp_ne_top

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Markov.lean

Modified Mathlib/MeasureTheory/Measure/Trim.lean

added theorem MeasureTheory.SigmaFinite.of_trim