LeanMachineLearning exposition

ProbabilityTheory.condDistrib_prod_left🔗

Minimal Lean file

condDistrib_prod_left🔗

LemmaProbabilityTheory.condDistrib_prod_left
Details

No docstring.

🔗theorem
ProbabilityTheory.condDistrib_prod_left.{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 Ω]
  [StandardBorelSpace Ω] [Nonempty Ω] {X : α → β} {Y : α → Ω}
  {T : α → γ} [MeasureTheory.IsFiniteMeasure μ] [StandardBorelSpace β]
  [Nonempty β] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
  (hT : AEMeasurable T μ) :
  ⇑𝓛[fun ω => (X ω, Y ω) | T; μ] =ᵐ[MeasureTheory.Measure.map T μ]
    ⇑(Kernel.compProd 𝓛[X | T; μ] 𝓛[Y | fun ω => (T ω, X ω); μ])
ProbabilityTheory.condDistrib_prod_left.{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 Ω]
  [StandardBorelSpace Ω] [Nonempty Ω]
  {X : α → β} {Y : α → Ω} {T : α → γ}
  [MeasureTheory.IsFiniteMeasure μ]
  [StandardBorelSpace β] [Nonempty β]
  (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ)
  (hT : AEMeasurable T μ) :
  ⇑𝓛[fun ω => (X ω, Y ω) | T;
        μ] =ᵐ[MeasureTheory.Measure.map T
      μ]
    ⇑(Kernel.compProd 𝓛[X | T; μ]
        𝓛[Y | fun ω => (T ω, X ω); μ])

Code

lemma condDistrib_prod_left [StandardBorelSpace β] [Nonempty β]
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hT : AEMeasurable T μ) :
    condDistrib (fun ω ↦ (X ω, Y ω)) T μ
      =ᵐ[μ.map T] condDistrib X T μ ⊗ₖ condDistrib Y (fun ω ↦ (T ω, X ω)) μ
Used by (3)

Actions: Source · Open Issue

Proof
by
  refine condDistrib_ae_eq_of_measure_eq_compProd (μ := μ) T (by fun_prop) ?_
  rw [← Measure.compProd_assoc', compProd_map_condDistrib hX, compProd_map_condDistrib hY,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
  rfl