Lemmas about measure composition-product #
theorem
MeasureTheory.Measure.AbsolutelyContinuous.compProd_left_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ η : ProbabilityTheory.Kernel α β}
{γ : Type u_3}
{mγ : MeasurableSpace γ}
[ProbabilityTheory.IsSFiniteKernel η]
{a : α}
(hac : (κ a).AbsolutelyContinuous (η a))
(ξ : ProbabilityTheory.Kernel (α × β) γ)
:
((κ.compProd ξ) a).AbsolutelyContinuous ((η.compProd ξ) a)