LeanMachineLearning exposition

ProbabilityTheory.indepFun_cond_of_indepFun🔗

Minimal Lean file

indepFun_cond_of_indepFun🔗

LemmaProbabilityTheory.indepFun_cond_of_indepFun
Details

No docstring.

🔗theorem
ProbabilityTheory.indepFun_cond_of_indepFun.{u_6, u_7, u_8}
  {α : Type u_6} {β : Type u_7} {γ : Type u_8} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → γ}
  (hXY : IndepFun X Y μ) (hY : Measurable Y) {s : Set γ}
  (hs : MeasurableSet s) : IndepFun X Y μ[|Y ⁻¹' s]
ProbabilityTheory.indepFun_cond_of_indepFun.{u_6,
    u_7, u_8}
  {α : Type u_6} {β : Type u_7}
  {γ : Type u_8} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → γ}
  (hXY : IndepFun X Y μ)
  (hY : Measurable Y) {s : Set γ}
  (hs : MeasurableSet s) :
  IndepFun X Y μ[|Y ⁻¹' s]

Code

lemma indepFun_cond_of_indepFun {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
    {mγ : MeasurableSpace γ} {μ : Measure α}
    {X : α → β} {Y : α → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y) {s : Set γ}
    (hs : MeasurableSet s) :
    X ⟂ᵢ[μ[|Y ⁻¹' s]] Y
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  by_cases h_zero : μ[|Y ⁻¹' s] = 0
  · simp [h_zero]
  rw [cond_eq_zero] at h_zero
  push Not at h_zero -- `h_zero : μ (Y ⁻¹' s) ≠ ⊤ ∧ μ (Y ⁻¹' s) ≠ 0`
  rw [indepFun_iff_measure_inter_preimage_eq_mul] at hXY ⊢
  intro u t hu ht
  rw [cond_apply (hs.preimage hY), cond_apply (hs.preimage hY), cond_apply (hs.preimage hY)]
  have h_eq : Y ⁻¹' s ∩ (X ⁻¹' u ∩ Y ⁻¹' t) = X ⁻¹' u ∩ Y ⁻¹' (s ∩ t) := by grind
  have hsu : μ (X ⁻¹' u ∩ Y ⁻¹' s) = μ (X ⁻¹' u) * μ (Y ⁻¹' s) := hXY u s hu hs
  rw [Set.inter_comm] at hsu
  have hust : μ (X ⁻¹' u ∩ Y ⁻¹' (s ∩ t)) = μ (X ⁻¹' u) * μ (Y ⁻¹' (s ∩ t)) :=
    hXY u (s ∩ t) hu (hs.inter ht)
  rw [hsu, h_eq, hust]
  simp_rw [mul_assoc]
  congr 1
  rw [← mul_assoc (μ (Y ⁻¹' s)), ENNReal.mul_inv_cancel h_zero.2 h_zero.1, one_mul]
  congr