LeanMachineLearning exposition

ProbabilityTheory.HasCondDistrib.prod🔗

Minimal Lean file

prod🔗

LemmaProbabilityTheory.HasCondDistrib.prod
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.prod.{u_1, u_2, u_4, u_5}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {Ω' : Type u_5}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  {Z : α → Ω'} {η : Kernel (β × Ω) Ω'} (h1 : HasCondDistrib Y X κ μ)
  (h2 : HasCondDistrib Z (fun ω => (X ω, Y ω)) η μ) :
  HasCondDistrib (fun ω => (Y ω, Z ω)) X (Kernel.compProd κ η) μ
ProbabilityTheory.HasCondDistrib.prod.{u_1,
    u_2, u_4, u_5}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {Ω' : Type u_5}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  {Z : α → Ω'} {η : Kernel (β × Ω) Ω'}
  (h1 : HasCondDistrib Y X κ μ)
  (h2 :
    HasCondDistrib Z (fun ω => (X ω, Y ω))
      η μ) :
  HasCondDistrib (fun ω => (Y ω, Z ω)) X
    (Kernel.compProd κ η) μ

Code

lemma HasCondDistrib.prod {Z : α → Ω'} {η : Kernel (β × Ω) Ω'}
    (h1 : HasCondDistrib Y X κ μ) (h2 : HasCondDistrib Z (fun ω ↦ (X ω, Y ω)) η μ) :
    HasCondDistrib (fun ω ↦ (Y ω, Z ω)) X (κ ⊗ₖ η) μ
Used by (2)

Actions: Source · Open Issue

Proof
by
  refine ⟨by fun_prop, ?_⟩
  rw [← Measure.compProd_assoc', ← h1.map_eq, ← h2.map_eq,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
  rfl