LeanMachineLearning exposition

ProbabilityTheory.HasLaw.prod_of_hasCondDistrib🔗

Minimal Lean file

prod_of_hasCondDistrib🔗

LemmaProbabilityTheory.HasLaw.prod_of_hasCondDistrib
Details

No docstring.

🔗theorem
ProbabilityTheory.HasLaw.prod_of_hasCondDistrib.{u_1, u_2, u_4}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  {P : MeasureTheory.Measure β} (h1 : HasLaw X P μ)
  (h2 : HasCondDistrib Y X κ μ) :
  HasLaw (fun ω => (X ω, Y ω)) (MeasureTheory.Measure.compProd P κ) μ
ProbabilityTheory.HasLaw.prod_of_hasCondDistrib.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  {P : MeasureTheory.Measure β}
  (h1 : HasLaw X P μ)
  (h2 : HasCondDistrib Y X κ μ) :
  HasLaw (fun ω => (X ω, Y ω))
    (MeasureTheory.Measure.compProd P κ) μ

Code

lemma HasLaw.prod_of_hasCondDistrib {P : Measure β}
    (h1 : HasLaw X P μ) (h2 : HasCondDistrib Y X κ μ) :
    HasLaw (fun ω ↦ (X ω, Y ω)) (P ⊗ₘ κ) μ
Used by (3)

Actions: Source · Open Issue

Proof
⟨by fun_prop, by rw [h2.map_eq, h1.map_eq]⟩