Commit 2023-06-19 04:18 fc574a23

View on Github →

feat: port Probability.Kernel.IntegralCompProd (#5140)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/IntegralCompProd.lean

added theorem MeasureTheory.AEStronglyMeasurable.compProd_mk_left

added theorem MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd

added theorem MeasureTheory.Integrable.compProd_mk_left_ae

added theorem MeasureTheory.Integrable.integral_compProd

added theorem MeasureTheory.Integrable.integral_norm_compProd

added theorem ProbabilityTheory.hasFiniteIntegral_compProd_iff'

added theorem ProbabilityTheory.hasFiniteIntegral_compProd_iff

added theorem ProbabilityTheory.hasFiniteIntegral_prod_mk_left

added theorem ProbabilityTheory.integrable_compProd_iff

added theorem ProbabilityTheory.integrable_kernel_prod_mk_left

added theorem ProbabilityTheory.integral_compProd

added theorem ProbabilityTheory.kernel.continuous_integral_integral

added theorem ProbabilityTheory.kernel.integral_fn_integral_add

added theorem ProbabilityTheory.kernel.integral_fn_integral_sub

added theorem ProbabilityTheory.kernel.integral_integral_add'

added theorem ProbabilityTheory.kernel.integral_integral_add

added theorem ProbabilityTheory.kernel.integral_integral_sub'

added theorem ProbabilityTheory.kernel.integral_integral_sub

added theorem ProbabilityTheory.kernel.lintegral_fn_integral_sub

added theorem ProbabilityTheory.set_integral_compProd

added theorem ProbabilityTheory.set_integral_compProd_univ_left

added theorem ProbabilityTheory.set_integral_compProd_univ_right