Commit 2021-10-01 20:35 75d022bb

View on Github →

feat(probability_theory/density): define probability density functions (#9323) This PR also proves some elementary properties about probability density function such as the law of the unconscious statistician.

Estimated changes

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.set_lintegral_lt_top_of_bdd_above

added theorem measure_theory.set_lintegral_lt_top_of_is_compact

added theorem measure_theory.set_lintegral_mono

added theorem measure_theory.set_lintegral_mono_ae

added theorem measure_theory.with_density_eq_zero

Created src/probability_theory/density.lean

added theorem measure_theory.has_pdf.measurable

added theorem measure_theory.map_eq_set_lintegral_pdf

added theorem measure_theory.map_eq_with_density_pdf

added theorem measure_theory.measurable_of_pdf_ne_zero

added theorem measure_theory.measurable_pdf

added theorem measure_theory.pdf.ae_lt_top

added theorem measure_theory.pdf.has_finite_integral_mul

added theorem measure_theory.pdf.has_pdf_iff

added theorem measure_theory.pdf.has_pdf_iff_of_measurable

added theorem measure_theory.pdf.have_lebesgue_decomposition_of_has_pdf

added theorem measure_theory.pdf.integrable_iff_integrable_mul_pdf

added theorem measure_theory.pdf.integral_fun_mul_eq_integral

added theorem measure_theory.pdf.integral_mul_eq_integral

added theorem measure_theory.pdf.lintegral_eq_measure_univ

added theorem measure_theory.pdf.map_absolutely_continuous

added theorem measure_theory.pdf.of_real_to_real_ae_eq

added theorem measure_theory.pdf.quasi_measure_preserving_has_pdf'

added theorem measure_theory.pdf.quasi_measure_preserving_has_pdf

added theorem measure_theory.pdf.real.has_pdf_iff

added theorem measure_theory.pdf.real.has_pdf_iff_of_measurable

added theorem measure_theory.pdf.to_quasi_measure_preserving

added def measure_theory.pdf

added theorem measure_theory.pdf_eq_zero_of_not_measurable

added theorem measure_theory.pdf_undef