Commit 2025-02-22 10:54 79f5daa1

View on Github →

feat(Probability): ae filter and integrability wrt a composition of kernel and measure (#22074)

Estimated changes

Modified Mathlib/Probability/Kernel/Composition/Basic.lean

added theorem ProbabilityTheory.Kernel.ae_ae_of_ae_comp

Modified Mathlib/Probability/Kernel/Composition/MeasureComp.lean

added theorem MeasureTheory.Measure.ae_ae_of_ae_comp

added theorem MeasureTheory.Measure.ae_integrable_of_integrable_comp

added theorem MeasureTheory.Measure.comp_compProd_comm

added theorem MeasureTheory.Measure.integrable_compProd_snd_iff

added theorem MeasureTheory.Measure.integrable_integral_norm_of_integrable_comp