LeanMachineLearning exposition

1.16. ForMathlib.Probability.Kernel.Composition.MeasureCompProd🔗

Lemmas about measure composition-product

Module LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MeasureCompProd contains 1 exposed declarations.

compProd_left_apply🔗

LemmaMeasureTheory.Measure.AbsolutelyContinuous.compProd_left_apply
Details

No docstring.

🔗theorem
MeasureTheory.Measure.AbsolutelyContinuous.compProd_left_apply.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {γ : Type u_3} {mγ : MeasurableSpace γ}
  [ProbabilityTheory.IsSFiniteKernel η] {a : α}
  (hac : AbsolutelyContinuous (κ a) (η a))
  (ξ : ProbabilityTheory.Kernel (α × β) γ) :
  AbsolutelyContinuous ((ProbabilityTheory.Kernel.compProd κ ξ) a)
    ((ProbabilityTheory.Kernel.compProd η ξ) a)
MeasureTheory.Measure.AbsolutelyContinuous.compProd_left_apply.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {κ η : ProbabilityTheory.Kernel α β}
  {γ : Type u_3} {mγ : MeasurableSpace γ}
  [ProbabilityTheory.IsSFiniteKernel η]
  {a : α}
  (hac : AbsolutelyContinuous (κ a) (η a))
  (ξ :
    ProbabilityTheory.Kernel (α × β) γ) :
  AbsolutelyContinuous
    ((ProbabilityTheory.Kernel.compProd κ
        ξ)
      a)
    ((ProbabilityTheory.Kernel.compProd η
        ξ)
      a)

Code

lemma AbsolutelyContinuous.compProd_left_apply {γ : Type*} {mγ : MeasurableSpace γ}
    [IsSFiniteKernel η] {a : α} (hac : κ a ≪ η a) (ξ : Kernel (α × β) γ) :
    (κ ⊗ₖ ξ) a ≪ (η ⊗ₖ ξ) a
Used by (1)

Actions: Source · Open Issue

Proof
by
  by_cases hκ : IsSFiniteKernel κ
  · by_cases hξ : IsSFiniteKernel ξ
    · simp_rw [Kernel.compProd_apply_eq_compProd_sectR, hac.compProd_left _]
    · simp [Kernel.compProd_of_not_isSFiniteKernel_right _ _ hξ]
  · simp [Kernel.compProd_of_not_isSFiniteKernel_left _ _ hκ]
  1. MeasureTheory.Measure.AbsolutelyContinuous.compProd_left_apply