LeanMachineLearning exposition

ProbabilityTheory.Measure.snd_compProd_prodMkLeft🔗

Minimal Lean file

snd_compProd_prodMkLeft🔗

LemmaProbabilityTheory.Measure.snd_compProd_prodMkLeft
Details

No docstring.

🔗theorem
ProbabilityTheory.Measure.snd_compProd_prodMkLeft.{u_7, u_8, u_9}
  {α : Type u_7} {β : Type u_8} {γ : Type u_9} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {μ : MeasureTheory.Measure (α × β)} [MeasureTheory.SFinite μ]
  {κ : Kernel β γ} [IsSFiniteKernel κ] :
  MeasureTheory.Measure.snd
      (MeasureTheory.Measure.compProd μ (Kernel.prodMkLeft α κ)) =
    MeasureTheory.Measure.bind (MeasureTheory.Measure.snd μ) ⇑κ
ProbabilityTheory.Measure.snd_compProd_prodMkLeft.{u_7,
    u_8, u_9}
  {α : Type u_7} {β : Type u_8}
  {γ : Type u_9} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {μ : MeasureTheory.Measure (α × β)}
  [MeasureTheory.SFinite μ]
  {κ : Kernel β γ} [IsSFiniteKernel κ] :
  MeasureTheory.Measure.snd
      (MeasureTheory.Measure.compProd μ
        (Kernel.prodMkLeft α κ)) =
    MeasureTheory.Measure.bind
      (MeasureTheory.Measure.snd μ) ⇑κ

Code

lemma Measure.snd_compProd_prodMkLeft {α β γ : Type*}
    {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
    {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] :
    (μ ⊗ₘ (κ.prodMkLeft α)).snd = κ ∘ₘ μ.snd

Actions: Source · Open Issue

Proof
by
  ext s hs
  rw [Measure.snd_apply hs, Measure.compProd_apply (hs.preimage (by fun_prop)),
    Measure.bind_apply hs (by fun_prop), Measure.snd,
    lintegral_map (κ.measurable_coe hs) (by fun_prop)]
  simp only [Kernel.prodMkLeft_apply]
  congr