LeanMachineLearning exposition

ProbabilityTheory.CondIndepFun.prod_right🔗

Minimal Lean file

prod_right🔗

LemmaProbabilityTheory.CondIndepFun.prod_right
Details

No docstring.

🔗theorem
ProbabilityTheory.CondIndepFun.prod_right.{u_1, u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4}
  {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} [MeasureTheory.IsFiniteMeasure μ]
  [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
  [StandardBorelSpace γ] [Nonempty γ] [StandardBorelSpace δ]
  [Nonempty δ] {X : α → β} {Y : α → γ} {Z : α → δ} (hX : Measurable X)
  (hY : Measurable Y) (hZ : Measurable Z)
  (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X Y μ) :
  CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X
    (fun ω => (Y ω, Z ω)) μ
ProbabilityTheory.CondIndepFun.prod_right.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {δ : Type u_4}
  {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  [MeasureTheory.IsFiniteMeasure μ]
  [StandardBorelSpace α]
  [StandardBorelSpace β] [Nonempty β]
  [StandardBorelSpace γ] [Nonempty γ]
  [StandardBorelSpace δ] [Nonempty δ]
  {X : α → β} {Y : α → γ} {Z : α → δ}
  (hX : Measurable X) (hY : Measurable Y)
  (hZ : Measurable Z)
  (h :
    CondIndepFun
      (MeasurableSpace.comap Z
        inferInstance)
      ⋯ X Y μ) :
  CondIndepFun
    (MeasurableSpace.comap Z
      inferInstance)
    ⋯ X (fun ω => (Y ω, Z ω)) μ

Code

lemma CondIndepFun.prod_right [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
    [StandardBorelSpace γ] [Nonempty γ] [StandardBorelSpace δ] [Nonempty δ]
    {X : α → β} {Y : α → γ} {Z : α → δ}
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (h : X ⟂ᵢ[Z, hZ; μ] Y) :
    X ⟂ᵢ[Z, hZ; μ] (fun ω ↦ (Y ω, Z ω))
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight hY hX hZ,
    condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h
  rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (by fun_prop) hX hZ,
    condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)]
  -- Key: condDistrib (Y, Z) Z μ z = (condDistrib Y Z μ z).map (y ↦ (y, z))
  have h_cond : condDistrib (fun ω ↦ (Y ω, Z ω)) Z μ =ᵐ[μ.map Z]
      fun z ↦ (condDistrib Y Z μ z).map (fun y ↦ (y, z)) := by
    suffices condDistrib (fun ω ↦ (Y ω, Z ω)) Z μ =ᵐ[μ.map Z]
        (condDistrib Y Z μ) ×ₖ Kernel.id by
      refine this.trans (ae_of_all _ fun x ↦ ?_)
      simp only
      rw [Kernel.prod_apply, Kernel.id_apply]
      ext s hs
      rw [Measure.map_apply (by fun_prop) hs, Measure.prod_apply_symm hs, lintegral_dirac]
    exact condDistrib_prod_self_left hY.aemeasurable hZ.aemeasurable
  -- Main calculation
  calc μ.map (fun x ↦ ((Z x, X x), (Y x, Z x)))
  _ = (μ.map (fun x ↦ ((Z x, X x), Y x))).map (fun p ↦ (p.1, (p.2, p.1.1))) := by
      rw [Measure.map_map (by fun_prop) (by fun_prop)]; rfl
  _ = (μ.map (fun ω ↦ (Z ω, X ω)) ⊗ₘ (condDistrib Y Z μ).prodMkRight β).map
        (fun p ↦ (p.1, (p.2, p.1.1))) := by rw [h]
  _ = μ.map (fun ω ↦ (Z ω, X ω)) ⊗ₘ (condDistrib (fun ω ↦ (Y ω, Z ω)) Z μ).prodMkRight β := by
    ext s hs
    rw [Measure.map_apply (by fun_prop) hs,
      Measure.compProd_apply (hs.preimage (by fun_prop)), Measure.compProd_apply hs]
    have h_cond' : ∀ᵐ p ∂(μ.map (fun ω ↦ (Z ω, X ω))),
        condDistrib (fun ω ↦ (Y ω, Z ω)) Z μ p.1 =
          (condDistrib Y Z μ p.1).map (fun y ↦ (y, p.1)) := by
      have h_fst : (μ.map (fun ω ↦ (Z ω, X ω))).map Prod.fst = μ.map Z := by
        rw [Measure.map_map (by fun_prop) (by fun_prop)]; rfl
      rw [← h_fst] at h_cond
      exact mem_ae_of_mem_ae_map (by fun_prop) h_cond
    refine lintegral_congr_ae (h_cond'.mono fun ⟨z, x⟩ hzx ↦ ?_)
    simp only [Kernel.prodMkRight_apply, hzx,
      Measure.map_apply (by fun_prop : Measurable fun y ↦ (y, z))
        (hs.preimage (by fun_prop : Measurable (Prod.mk (z, x))))]
    congr 1