Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-23 08:35 c0d694db

View on Github →

feat(probability/kernel/integral_comp_prod): Bochner integral against the composition-product of two kernels (#18976)

Estimated changes

Modified src/probability/kernel/composition.lean

added theorem probability_theory.kernel.ae_ae_of_ae_comp_prod

added theorem probability_theory.kernel.ae_kernel_lt_top

added theorem probability_theory.kernel.ae_null_of_comp_prod_null

added theorem probability_theory.kernel.comp_prod_null

added theorem probability_theory.kernel.comp_prod_restrict

added theorem probability_theory.kernel.comp_prod_restrict_left

added theorem probability_theory.kernel.comp_prod_restrict_right

added theorem probability_theory.kernel.le_comp_prod_apply

added theorem probability_theory.kernel.lintegral_comp_prod₀

added theorem probability_theory.kernel.set_lintegral_comp_prod

added theorem probability_theory.kernel.set_lintegral_comp_prod_univ_left

added theorem probability_theory.kernel.set_lintegral_comp_prod_univ_right

Created src/probability/kernel/integral_comp_prod.lean

added theorem measure_theory.ae_strongly_measurable.comp_prod_mk_left

added theorem measure_theory.ae_strongly_measurable.integral_kernel_comp_prod

added theorem measure_theory.integrable.comp_prod_mk_left_ae

added theorem measure_theory.integrable.integral_comp_prod

added theorem measure_theory.integrable.integral_norm_comp_prod

added theorem probability_theory.has_finite_integral_comp_prod_iff'

added theorem probability_theory.has_finite_integral_comp_prod_iff

added theorem probability_theory.has_finite_integral_prod_mk_left

added theorem probability_theory.integrable_comp_prod_iff

added theorem probability_theory.integrable_kernel_prod_mk_left

added theorem probability_theory.integral_comp_prod

added theorem probability_theory.kernel.continuous_integral_integral

added theorem probability_theory.kernel.integral_fn_integral_add

added theorem probability_theory.kernel.integral_fn_integral_sub

added theorem probability_theory.kernel.integral_integral_add'

added theorem probability_theory.kernel.integral_integral_add

added theorem probability_theory.kernel.integral_integral_sub'

added theorem probability_theory.kernel.integral_integral_sub

added theorem probability_theory.kernel.lintegral_fn_integral_sub

added theorem probability_theory.set_integral_comp_prod

added theorem probability_theory.set_integral_comp_prod_univ_left

added theorem probability_theory.set_integral_comp_prod_univ_right

Modified src/probability/kernel/with_density.lean

added theorem probability_theory.kernel.integral_with_density