LeanMachineLearning exposition

ProbabilityTheory.Measure.snd_prodAssoc_compProd_prodMkLeft🔗

Minimal Lean file

snd_prodAssoc_compProd_prodMkLeft🔗

LemmaProbabilityTheory.Measure.snd_prodAssoc_compProd_prodMkLeft
Details

No docstring.

🔗theorem
ProbabilityTheory.Measure.snd_prodAssoc_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.map (⇑MeasurableEquiv.prodAssoc)
        (MeasureTheory.Measure.compProd μ (Kernel.prodMkLeft α κ))) =
    MeasureTheory.Measure.compProd (MeasureTheory.Measure.snd μ) κ
ProbabilityTheory.Measure.snd_prodAssoc_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.map
        (⇑MeasurableEquiv.prodAssoc)
        (MeasureTheory.Measure.compProd μ
          (Kernel.prodMkLeft α κ))) =
    MeasureTheory.Measure.compProd
      (MeasureTheory.Measure.snd μ) κ

Code

lemma Measure.snd_prodAssoc_compProd_prodMkLeft {α β γ : Type*}
    {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
    {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] :
    (((μ ⊗ₘ (κ.prodMkLeft α))).map MeasurableEquiv.prodAssoc).snd = μ.snd ⊗ₘ κ
Used by (1)

Actions: Source · Open Issue

Proof
by
  ext s hs
  rw [Measure.snd_apply hs, Measure.map_apply (by fun_prop) (hs.preimage (by fun_prop)),
    Measure.compProd_apply, Measure.compProd_apply hs, Measure.snd, lintegral_map _ (by fun_prop)]
  · simp only [Kernel.prodMkLeft_apply]
    congr
  · exact Kernel.measurable_kernel_prodMk_left hs
  · exact hs.preimage (by fun_prop)