Commit 2024-11-05 08:41 55a3a269

View on Github →

refactor(HasPDF): use structure fields (#18371) ... instead of a single field with Ands. Also drop an AEMeasurable assumption that follows from HasPDF.

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

modified theorem MeasureTheory.integrable_rnDeriv_smul_iff

modified theorem MeasureTheory.integral_rnDeriv_smul

modified theorem MeasureTheory.setIntegral_rnDeriv_smul

modified theorem MeasureTheory.withDensityᵥ_rnDeriv_smul

Modified Mathlib/Probability/Density.lean

modified theorem MeasureTheory.HasPDF.absolutelyContinuous

modified theorem MeasureTheory.HasPDF.aemeasurable

deleted theorem MeasureTheory.HasPDF.congr'

modified theorem MeasureTheory.HasPDF.congr

added theorem MeasureTheory.HasPDF.congr_iff

modified theorem MeasureTheory.hasPDF_iff

modified theorem MeasureTheory.hasPDF_iff_of_aemeasurable

modified theorem MeasureTheory.hasPDF_of_map_eq_withDensity

modified theorem MeasureTheory.pdf.integral_pdf_smul

modified theorem MeasureTheory.pdf.quasiMeasurePreserving_hasPDF'

modified theorem MeasureTheory.pdf.quasiMeasurePreserving_hasPDF

deleted theorem Real.hasPDF_iff