Mathlib Changelog
v4
Changelog
About
Github
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