Commit 2023-10-30 13:56 185dddfc

View on Github →

feat: if X is Gaussian, then X+y and c*X are Gaussian (#7674)

Estimated changes

Modified Mathlib/Algebra/NeZero.lean

added theorem neZero_zero_iff_false

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

added theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul'

added theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul

added theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul

added theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul'

added theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul

added theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

added theorem aemeasurable_of_map_neZero

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

added theorem MeasureTheory.Measure.map_const

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Probability/Distributions/Gaussian.lean

added theorem MeasurableEmbedding.gaussianReal_comap_apply

added theorem MeasurableEquiv.gaussianReal_map_symm_apply

added theorem ProbabilityTheory.gaussianPdfReal_add

added theorem ProbabilityTheory.gaussianPdfReal_inv_mul

added theorem ProbabilityTheory.gaussianPdfReal_mul

added theorem ProbabilityTheory.gaussianPdfReal_sub

added theorem ProbabilityTheory.gaussianReal_add_const

added theorem ProbabilityTheory.gaussianReal_const_add

added theorem ProbabilityTheory.gaussianReal_const_mul

added theorem ProbabilityTheory.gaussianReal_map_add_const

added theorem ProbabilityTheory.gaussianReal_map_const_add

added theorem ProbabilityTheory.gaussianReal_map_const_mul

added theorem ProbabilityTheory.gaussianReal_map_mul_const

added theorem ProbabilityTheory.gaussianReal_mul_const