LeanMachineLearning exposition

ProbabilityTheory.cond_of_condIndepFun🔗

Minimal Lean file

cond_of_condIndepFun🔗

LemmaProbabilityTheory.cond_of_condIndepFun
Details

No docstring.

🔗theorem
ProbabilityTheory.cond_of_condIndepFun.{u_1, u_2, u_5, u_6}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_5} {Ω' : Type u_6}
  {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β} [MeasurableSpace Ω] [StandardBorelSpace Ω]
  [Nonempty Ω] [mΩ' : MeasurableSpace Ω'] [StandardBorelSpace Ω']
  {X : α → β} {Y : α → Ω} {Z : α → Ω'} [StandardBorelSpace α]
  [StandardBorelSpace β] [Nonempty β] [Countable β] [Countable Ω']
  [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hZ : Measurable Z)
  (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ Y X μ)
  (hX : Measurable X) (hY : Measurable Y) {b : β} {ω : Ω'}
  (hμ : μ (Z ⁻¹' {ω} ∩ X ⁻¹' {b}) ≠ 0) :
  𝓛[Y | Z ⁻¹' {ω} ∩ X ⁻¹' {b}; μ] = 𝓛[Y | Z in {ω}; μ]
ProbabilityTheory.cond_of_condIndepFun.{u_1,
    u_2, u_5, u_6}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_5} {Ω' : Type u_6}
  {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace Ω]
  [StandardBorelSpace Ω] [Nonempty Ω]
  [mΩ' : MeasurableSpace Ω']
  [StandardBorelSpace Ω'] {X : α → β}
  {Y : α → Ω} {Z : α → Ω'}
  [StandardBorelSpace α]
  [StandardBorelSpace β] [Nonempty β]
  [Countable β] [Countable Ω']
  [MeasureTheory.IsZeroOrProbabilityMeasure
      μ]
  (hZ : Measurable Z)
  (h :
    CondIndepFun
      (MeasurableSpace.comap Z
        inferInstance)
      ⋯ Y X μ)
  (hX : Measurable X) (hY : Measurable Y)
  {b : β} {ω : Ω'}
  (hμ : μ (Z ⁻¹' {ω} ∩ X ⁻¹' {b}) ≠ 0) :
  𝓛[Y | Z ⁻¹' {ω} ∩ X ⁻¹' {b}; μ] =
    𝓛[Y | Z in {ω}; μ]

Code

lemma cond_of_condIndepFun [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β] [Countable β]
    [Countable Ω']
    [IsZeroOrProbabilityMeasure μ]
    (hZ : Measurable Z)
    (h : CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le Y X μ)
    (hX : Measurable X) (hY : Measurable Y) {b : β} {ω : Ω'}
    (hμ : μ (Z ⁻¹' {ω} ∩ X ⁻¹' {b}) ≠ 0) :
    (μ[|Z ⁻¹' {ω} ∩ X ⁻¹' {b}]).map Y = (μ[|Z ⁻¹' {ω}]).map Y
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  symm at h
  have h := (condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight hY hX hZ).mp h
  have h_left := condDistrib_ae_eq_cond (hZ.prodMk hX) hY (μ := μ)
  have h_right := condDistrib_ae_eq_cond hZ hY (μ := μ)
  rw [Filter.EventuallyEq, ae_iff_of_countable] at h h_left h_right
  specialize h (ω, b)
  specialize h_left (ω, b)
  specialize h_right ω
  rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at h h_left h_right
  rw [← Set.singleton_prod_singleton, Set.mk_preimage_prod] at h h_left
  have hZ_ne : μ (Z ⁻¹' {ω}) ≠ 0 := fun h ↦ hμ (measure_mono_null Set.inter_subset_left h)
  rw [← h_right hZ_ne, ← h_left hμ, h hμ]
  simp