Commit 2024-07-12 23:56 8e7020a5

View on Github →

feat(MeasureTheory): drop measurability assumptions here and there (#14680)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

deleted theorem MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_stronglyMeasurable

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

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

modified theorem MeasureTheory.setLIntegral_lt_top_of_isCompact

added theorem MeasureTheory.setLIntegral_lt_top_of_le_nnreal

modified theorem MeasureTheory.setLIntegral_mono

modified theorem MeasureTheory.setLIntegral_mono_ae

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

modified theorem MeasureTheory.setIntegral_gt_gt

Modified Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean

Modified Mathlib/MeasureTheory/Measure/Tilted.lean

modified theorem MeasureTheory.rnDeriv_tilted_left

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

deleted theorem MeasureTheory.SigmaFinite.withDensity

deleted theorem MeasureTheory.SigmaFinite.withDensity_ofReal

modified theorem MeasureTheory.SigmaFinite.withDensity_of_ne_top'

deleted theorem MeasureTheory.withDensity_eq_zero

Modified Mathlib/MeasureTheory/Measure/WithDensityFinite.lean

Modified Mathlib/Probability/Kernel/Disintegration/CondCdf.lean