Commit 2023-06-12 20:15 42b5fd46

View on Github →

feat: port Probability.Density (#4962)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Density.lean

added theorem MeasureTheory.HasPDF.measurable

added theorem MeasureTheory.hasPDF_of_pdf_ne_zero

added theorem MeasureTheory.map_eq_set_lintegral_pdf

added theorem MeasureTheory.map_eq_withDensity_pdf

added theorem MeasureTheory.measurable_of_pdf_ne_zero

added theorem MeasureTheory.measurable_pdf

added theorem MeasureTheory.pdf.IsUniform.hasPDF

added theorem MeasureTheory.pdf.IsUniform.integral_eq

added theorem MeasureTheory.pdf.IsUniform.isProbabilityMeasure

added theorem MeasureTheory.pdf.IsUniform.measure_preimage

added theorem MeasureTheory.pdf.IsUniform.mul_pdf_integrable

added theorem MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eq

added def MeasureTheory.pdf.IsUniform

added theorem MeasureTheory.pdf.hasFiniteIntegral_mul

added theorem MeasureTheory.pdf.hasPDF_iff

added theorem MeasureTheory.pdf.hasPDF_iff_of_measurable

added theorem MeasureTheory.pdf.haveLebesgueDecomposition_of_hasPDF

added theorem MeasureTheory.pdf.integrable_iff_integrable_mul_pdf

added theorem MeasureTheory.pdf.integral_fun_mul_eq_integral

added theorem MeasureTheory.pdf.integral_mul_eq_integral

added theorem MeasureTheory.pdf.lintegral_eq_measure_univ

added theorem MeasureTheory.pdf.map_absolutelyContinuous

added theorem MeasureTheory.pdf.quasiMeasurePreserving_hasPDF'

added theorem MeasureTheory.pdf.quasiMeasurePreserving_hasPDF

added theorem MeasureTheory.pdf.to_quasiMeasurePreserving

added def MeasureTheory.pdf

added theorem MeasureTheory.pdf_eq_zero_of_not_measurable

added theorem MeasureTheory.pdf_undef

added theorem Real.hasPDF_iff