LeanMachineLearning exposition

ProbabilityTheory.fst_condDistrib_prod🔗

Minimal Lean file

fst_condDistrib_prod🔗

LemmaProbabilityTheory.fst_condDistrib_prod
Details

No docstring.

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

Code

lemma fst_condDistrib_prod [StandardBorelSpace β] [Nonempty β]
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hT : AEMeasurable T μ) :
    (condDistrib (fun ω ↦ (X ω, Y ω)) T μ).fst =ᵐ[μ.map T] condDistrib X T μ
Body uses (1)

Actions: Source · Open Issue

Proof
by
  filter_upwards [condDistrib_prod_left hX hY hT] with c hc
  rw [Kernel.fst_apply, hc, ← Kernel.fst_apply, Kernel.fst_compProd]