LeanMachineLearning exposition

ProbabilityTheory.indepFun_fst_prod🔗

Minimal Lean file

indepFun_fst_prod🔗

LemmaProbabilityTheory.indepFun_fst_prod
Details

No docstring.

🔗theorem
ProbabilityTheory.indepFun_fst_prod.{u_1, u_2, u_3, u_5} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} {Ω : Type u_5} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [MeasurableSpace Ω] {X : α → β} {Y : α → Ω}
  [MeasureTheory.IsFiniteMeasure μ] (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ) (h_indep : IndepFun X Y μ)
  (ν : MeasureTheory.Measure γ) [MeasureTheory.IsProbabilityMeasure ν] :
  IndepFun (fun ω => X (Prod.fst ω)) (fun ω => Y (Prod.fst ω))
    (MeasureTheory.Measure.prod μ ν)
ProbabilityTheory.indepFun_fst_prod.{u_1,
    u_2, u_3, u_5}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {Ω : Type u_5}
  {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  [MeasurableSpace Ω] {X : α → β}
  {Y : α → Ω}
  [MeasureTheory.IsFiniteMeasure μ]
  (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ)
  (h_indep : IndepFun X Y μ)
  (ν : MeasureTheory.Measure γ)
  [MeasureTheory.IsProbabilityMeasure ν] :
  IndepFun (fun ω => X (Prod.fst ω))
    (fun ω => Y (Prod.fst ω))
    (MeasureTheory.Measure.prod μ ν)

Code

lemma indepFun_fst_prod (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (h_indep : IndepFun X Y μ)
    (ν : Measure γ) [IsProbabilityMeasure ν] :
    IndepFun (fun ω ↦ X ω.1) (fun ω ↦ Y ω.1) (μ.prod ν)

Actions: Source · Open Issue

Proof
by
  rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop)] at h_indep ⊢
  have :  AEMeasurable (fun ω ↦ (X ω, Y ω)) (Measure.map Prod.fst (μ.prod ν)) := by
    simp only [Measure.map_fst_prod, measure_univ, one_smul]
    fun_prop
  have :  AEMeasurable X (Measure.map Prod.fst (μ.prod ν)) := by
    simp only [Measure.map_fst_prod, measure_univ, one_smul]
    fun_prop
  have :  AEMeasurable Y (Measure.map Prod.fst (μ.prod ν)) := by
    simp only [Measure.map_fst_prod, measure_univ, one_smul]
    fun_prop
  have h : (μ.prod ν).map (fun ω ↦ (X ω.1, Y ω.1)) = μ.map (fun ω ↦ (X ω, Y ω)) := by
    conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst,
      AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    rfl
  rw [h, h_indep]
  conv_lhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst,
      AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop),
      AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
  rfl