Commit 2024-03-10 07:58 6406e752

View on Github →

feat(Probability/Kernel): add compProd_add_left/right (#11272) Interaction of the composition-product of kernels with addition.

Estimated changes

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.kernel.const_add

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.kernel.compProd_add_left

added theorem ProbabilityTheory.kernel.compProd_add_right

added theorem ProbabilityTheory.kernel.prodMkLeft_add

added theorem ProbabilityTheory.kernel.prodMkRight_add

Modified Mathlib/Probability/Kernel/MeasureCompProd.lean

added theorem MeasureTheory.Measure.compProd_add_left

added theorem MeasureTheory.Measure.compProd_add_right

added theorem MeasureTheory.Measure.compProd_apply_prod