LeanMachineLearning exposition

1.10. ForMathlib.Probability.Independence.CondIndepFun🔗

Laws of stepsUntil and rewardByCount

Module LeanMachineLearning.ForMathlib.Probability.Independence.CondIndepFun contains 10 exposed declarations.

of_prod_right🔗

LemmaProbabilityTheory.Kernel.IndepFun.of_prod_right
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.IndepFun.of_prod_right.{u_1, u_2, u_3, u_7,
    u_8}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {ε : Type u_7}
  {Ω : Type u_8} {mΩ : MeasurableSpace Ω} {mε : MeasurableSpace ε}
  {μ : MeasureTheory.Measure Ω} {κ : Kernel Ω α} {X : α → β} {Y : α → γ}
  {T : α → ε} (h : IndepFun X (fun ω => (Y ω, T ω)) κ μ) :
  IndepFun X Y κ μ
ProbabilityTheory.Kernel.IndepFun.of_prod_right.{u_1,
    u_2, u_3, u_7, u_8}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {ε : Type u_7}
  {Ω : Type u_8} {mΩ : MeasurableSpace Ω}
  {mε : MeasurableSpace ε}
  {μ : MeasureTheory.Measure Ω}
  {κ : Kernel Ω α} {X : α → β} {Y : α → γ}
  {T : α → ε}
  (h :
    IndepFun X (fun ω => (Y ω, T ω)) κ
      μ) :
  IndepFun X Y κ μ

Code

lemma Kernel.IndepFun.of_prod_right {ε Ω : Type*} {mΩ : MeasurableSpace Ω} {mε : MeasurableSpace ε}
    {μ : Measure Ω} {κ : Kernel Ω α} {X : α → β} {Y : α → γ} {T : α → ε}
    (h : IndepFun X (fun ω ↦ (Y ω, T ω)) κ μ) :
    IndepFun X Y κ μ
Used by (2)

Actions: Source · Open Issue

Proof
by
  rw [Kernel.indepFun_iff_measure_inter_preimage_eq_mul] at h ⊢
  intro s t hs ht
  specialize h s (t ×ˢ .univ) hs (ht.prod .univ)
  simpa [Set.mk_preimage_prod] using h

of_prod_left🔗

LemmaProbabilityTheory.Kernel.IndepFun.of_prod_left
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.IndepFun.of_prod_left.{u_1, u_2, u_3, u_7, u_8}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {ε : Type u_7}
  {Ω : Type u_8} {mΩ : MeasurableSpace Ω} {mε : MeasurableSpace ε}
  {μ : MeasureTheory.Measure Ω} {κ : Kernel Ω α} {X : α → β} {Y : α → γ}
  {T : α → ε} (h : IndepFun (fun ω => (X ω, T ω)) Y κ μ) :
  IndepFun X Y κ μ
ProbabilityTheory.Kernel.IndepFun.of_prod_left.{u_1,
    u_2, u_3, u_7, u_8}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {ε : Type u_7}
  {Ω : Type u_8} {mΩ : MeasurableSpace Ω}
  {mε : MeasurableSpace ε}
  {μ : MeasureTheory.Measure Ω}
  {κ : Kernel Ω α} {X : α → β} {Y : α → γ}
  {T : α → ε}
  (h :
    IndepFun (fun ω => (X ω, T ω)) Y κ
      μ) :
  IndepFun X Y κ μ

Code

lemma Kernel.IndepFun.of_prod_left {ε Ω : Type*} {mΩ : MeasurableSpace Ω} {mε : MeasurableSpace ε}
    {μ : Measure Ω} {κ : Kernel Ω α} {X : α → β} {Y : α → γ} {T : α → ε}
    (h : IndepFun (fun ω ↦ (X ω, T ω)) Y κ μ) :
    IndepFun X Y κ μ
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
h.symm.of_prod_right.symm

of_prod_right🔗

LemmaProbabilityTheory.CondIndepFun.of_prod_right
Details

No docstring.

🔗theorem
ProbabilityTheory.CondIndepFun.of_prod_right.{u_1, u_2, u_3, u_4, u_7}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
  {μ : MeasureTheory.Measure α} {ε : Type u_7} {mε : MeasurableSpace ε}
  [StandardBorelSpace α] [MeasureTheory.IsFiniteMeasure μ] {X : α → β}
  {Y : α → γ} {Z : α → δ} {T : α → ε} (hZ : Measurable Z)
  (h :
    CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X
      (fun ω => (Y ω, T ω)) μ) :
  CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X Y μ
ProbabilityTheory.CondIndepFun.of_prod_right.{u_1,
    u_2, u_3, u_4, u_7}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {δ : Type u_4}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {μ : MeasureTheory.Measure α}
  {ε : Type u_7} {mε : MeasurableSpace ε}
  [StandardBorelSpace α]
  [MeasureTheory.IsFiniteMeasure μ]
  {X : α → β} {Y : α → γ} {Z : α → δ}
  {T : α → ε} (hZ : Measurable Z)
  (h :
    CondIndepFun
      (MeasurableSpace.comap Z
        inferInstance)
      ⋯ X (fun ω => (Y ω, T ω)) μ) :
  CondIndepFun
    (MeasurableSpace.comap Z
      inferInstance)
    ⋯ X Y μ

Code

lemma CondIndepFun.of_prod_right {ε : Type*} {mε : MeasurableSpace ε}
    [StandardBorelSpace α] [IsFiniteMeasure μ]
    {X : α → β} {Y : α → γ} {Z : α → δ} {T : α → ε} (hZ : Measurable Z)
    (h : X ⟂ᵢ[Z, hZ; μ] (fun ω ↦ (Y ω, T ω))) :
    X ⟂ᵢ[Z, hZ; μ] Y
Body uses (1)

Actions: Source · Open Issue

Proof
Kernel.IndepFun.of_prod_right h

of_prod_left🔗

LemmaProbabilityTheory.CondIndepFun.of_prod_left
Details

No docstring.

🔗theorem
ProbabilityTheory.CondIndepFun.of_prod_left.{u_1, u_2, u_3, u_4, u_7}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
  {μ : MeasureTheory.Measure α} {ε : Type u_7} {mε : MeasurableSpace ε}
  [StandardBorelSpace α] [MeasureTheory.IsFiniteMeasure μ] {X : α → β}
  {Y : α → γ} {Z : α → δ} {T : α → ε} (hZ : Measurable Z)
  (h :
    CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯
      (fun ω => (X ω, T ω)) Y μ) :
  CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X Y μ
ProbabilityTheory.CondIndepFun.of_prod_left.{u_1,
    u_2, u_3, u_4, u_7}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {δ : Type u_4}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {μ : MeasureTheory.Measure α}
  {ε : Type u_7} {mε : MeasurableSpace ε}
  [StandardBorelSpace α]
  [MeasureTheory.IsFiniteMeasure μ]
  {X : α → β} {Y : α → γ} {Z : α → δ}
  {T : α → ε} (hZ : Measurable Z)
  (h :
    CondIndepFun
      (MeasurableSpace.comap Z
        inferInstance)
      ⋯ (fun ω => (X ω, T ω)) Y μ) :
  CondIndepFun
    (MeasurableSpace.comap Z
      inferInstance)
    ⋯ X Y μ

Code

lemma CondIndepFun.of_prod_left {ε : Type*} {mε : MeasurableSpace ε}
    [StandardBorelSpace α] [IsFiniteMeasure μ]
    {X : α → β} {Y : α → γ} {Z : α → δ} {T : α → ε} (hZ : Measurable Z)
    (h : (fun ω ↦ (X ω, T ω)) ⟂ᵢ[Z, hZ; μ] Y) :
    X ⟂ᵢ[Z, hZ; μ] Y
Body uses (1)

Actions: Source · Open Issue

Proof
Kernel.IndepFun.of_prod_left h

of_measurable🔗

LemmaProbabilityTheory.IndepFun.of_measurable
Details

No docstring.

🔗theorem
ProbabilityTheory.IndepFun.of_measurable.{u_1, u_3, u_4, u_5, u_6}
  {α : Type u_1} {γ : Type u_3} {δ : Type u_4} {γ' : Type u_5}
  {δ' : Type u_6} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} {mγ' : MeasurableSpace γ'}
  {mδ' : MeasurableSpace δ'} [StandardBorelSpace δ'] [Nonempty δ']
  [StandardBorelSpace γ'] [Nonempty γ'] {μ : MeasureTheory.Measure α}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'} {Z' : α → δ'}
  (h_indep : IndepFun Y Z μ) (hY_meas : Measurable Y')
  (hZ_meas : Measurable Z') : IndepFun Y' Z' μ
ProbabilityTheory.IndepFun.of_measurable.{u_1,
    u_3, u_4, u_5, u_6}
  {α : Type u_1} {γ : Type u_3}
  {δ : Type u_4} {γ' : Type u_5}
  {δ' : Type u_6} {mα : MeasurableSpace α}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {mγ' : MeasurableSpace γ'}
  {mδ' : MeasurableSpace δ'}
  [StandardBorelSpace δ'] [Nonempty δ']
  [StandardBorelSpace γ'] [Nonempty γ']
  {μ : MeasureTheory.Measure α}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'}
  {Z' : α → δ'} (h_indep : IndepFun Y Z μ)
  (hY_meas : Measurable Y')
  (hZ_meas : Measurable Z') :
  IndepFun Y' Z' μ

Code

lemma IndepFun.of_measurable (h_indep : Y ⟂ᵢ[μ] Z)
    (hY_meas : Measurable[mγ.comap Y] Y') (hZ_meas : Measurable[mδ.comap Z] Z') :
    Y' ⟂ᵢ[μ] Z'

Actions: Source · Open Issue

Proof
by
  obtain ⟨φ, hφ_meas, h_eqY⟩ : ∃ φ, Measurable φ ∧ Y' = φ ∘ Y := hY_meas.exists_eq_measurable_comp
  obtain ⟨ψ, hψ_meas, h_eqZ⟩ : ∃ ψ, Measurable ψ ∧ Z' = ψ ∘ Z := hZ_meas.exists_eq_measurable_comp
  rw [h_eqY, h_eqZ]
  exact h_indep.comp hφ_meas hψ_meas

of_measurable_left🔗

LemmaProbabilityTheory.IndepFun.of_measurable_left
Details

No docstring.

🔗theorem
ProbabilityTheory.IndepFun.of_measurable_left.{u_1, u_3, u_4, u_5}
  {α : Type u_1} {γ : Type u_3} {δ : Type u_4} {γ' : Type u_5}
  {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} {mγ' : MeasurableSpace γ'}
  [StandardBorelSpace γ'] [Nonempty γ'] {μ : MeasureTheory.Measure α}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'} (h_indep : IndepFun Y Z μ)
  (hY_meas : Measurable Y') : IndepFun Y' Z μ
ProbabilityTheory.IndepFun.of_measurable_left.{u_1,
    u_3, u_4, u_5}
  {α : Type u_1} {γ : Type u_3}
  {δ : Type u_4} {γ' : Type u_5}
  {mα : MeasurableSpace α}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {mγ' : MeasurableSpace γ'}
  [StandardBorelSpace γ'] [Nonempty γ']
  {μ : MeasureTheory.Measure α}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'}
  (h_indep : IndepFun Y Z μ)
  (hY_meas : Measurable Y') :
  IndepFun Y' Z μ

Code

lemma IndepFun.of_measurable_left
    (h_indep : Y ⟂ᵢ[μ] Z) (hY_meas : Measurable[mγ.comap Y] Y') :
    Y' ⟂ᵢ[μ] Z

Actions: Source · Open Issue

Proof
by
  obtain ⟨φ, hφ_meas, h_eqY⟩ : ∃ φ, Measurable φ ∧ Y' = φ ∘ Y := hY_meas.exists_eq_measurable_comp
  rw [h_eqY]
  exact h_indep.comp hφ_meas measurable_id

of_measurable_right🔗

LemmaProbabilityTheory.IndepFun.of_measurable_right
Details

No docstring.

🔗theorem
ProbabilityTheory.IndepFun.of_measurable_right.{u_1, u_3, u_4, u_6}
  {α : Type u_1} {γ : Type u_3} {δ : Type u_4} {δ' : Type u_6}
  {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} {mδ' : MeasurableSpace δ'}
  [StandardBorelSpace δ'] [Nonempty δ'] {μ : MeasureTheory.Measure α}
  {Y : α → γ} {Z : α → δ} {Z' : α → δ'} (h_indep : IndepFun Y Z μ)
  (hZ_meas : Measurable Z') : IndepFun Y Z' μ
ProbabilityTheory.IndepFun.of_measurable_right.{u_1,
    u_3, u_4, u_6}
  {α : Type u_1} {γ : Type u_3}
  {δ : Type u_4} {δ' : Type u_6}
  {mα : MeasurableSpace α}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {mδ' : MeasurableSpace δ'}
  [StandardBorelSpace δ'] [Nonempty δ']
  {μ : MeasureTheory.Measure α}
  {Y : α → γ} {Z : α → δ} {Z' : α → δ'}
  (h_indep : IndepFun Y Z μ)
  (hZ_meas : Measurable Z') :
  IndepFun Y Z' μ

Code

lemma IndepFun.of_measurable_right
    (h_indep : Y ⟂ᵢ[μ] Z) (hZ_meas : Measurable[mδ.comap Z] Z') :
    Y ⟂ᵢ[μ] Z'
Used by (3)

Actions: Source · Open Issue

Proof
by
  obtain ⟨ψ, hψ_meas, h_eqZ⟩ : ∃ ψ, Measurable ψ ∧ Z' = ψ ∘ Z := hZ_meas.exists_eq_measurable_comp
  rw [h_eqZ]
  exact h_indep.comp measurable_id hψ_meas

of_measurable🔗

LemmaProbabilityTheory.CondIndepFun.of_measurable
Details

No docstring.

🔗theorem
ProbabilityTheory.CondIndepFun.of_measurable.{u_1, u_2, u_3, u_4, u_5,
    u_6}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4}
  {γ' : Type u_5} {δ' : Type u_6} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} {mγ' : MeasurableSpace γ'}
  {mδ' : MeasurableSpace δ'} [StandardBorelSpace δ'] [Nonempty δ']
  [StandardBorelSpace γ'] [Nonempty γ'] {μ : MeasureTheory.Measure α}
  {X : α → β} {hX : Measurable X} {Y : α → γ} {Z : α → δ} {Y' : α → γ'}
  {Z' : α → δ'} [StandardBorelSpace α] [MeasureTheory.IsFiniteMeasure μ]
  (h_indep :
    CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y Z μ)
  (hY_meas : Measurable Y') (hZ_meas : Measurable Z') :
  CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y' Z' μ
ProbabilityTheory.CondIndepFun.of_measurable.{u_1,
    u_2, u_3, u_4, u_5, u_6}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {δ : Type u_4}
  {γ' : Type u_5} {δ' : Type u_6}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {mγ' : MeasurableSpace γ'}
  {mδ' : MeasurableSpace δ'}
  [StandardBorelSpace δ'] [Nonempty δ']
  [StandardBorelSpace γ'] [Nonempty γ']
  {μ : MeasureTheory.Measure α}
  {X : α → β} {hX : Measurable X}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'}
  {Z' : α → δ'} [StandardBorelSpace α]
  [MeasureTheory.IsFiniteMeasure μ]
  (h_indep :
    CondIndepFun
      (MeasurableSpace.comap X
        inferInstance)
      ⋯ Y Z μ)
  (hY_meas : Measurable Y')
  (hZ_meas : Measurable Z') :
  CondIndepFun
    (MeasurableSpace.comap X
      inferInstance)
    ⋯ Y' Z' μ

Code

lemma CondIndepFun.of_measurable (h_indep : Y ⟂ᵢ[X, hX; μ] Z)
    (hY_meas : Measurable[mγ.comap Y] Y') (hZ_meas : Measurable[mδ.comap Z] Z') :
    Y' ⟂ᵢ[X, hX; μ] Z'

Actions: Source · Open Issue

Proof
by
  obtain ⟨φ, hφ_meas, h_eqY⟩ : ∃ φ, Measurable φ ∧ Y' = φ ∘ Y := hY_meas.exists_eq_measurable_comp
  obtain ⟨ψ, hψ_meas, h_eqZ⟩ : ∃ ψ, Measurable ψ ∧ Z' = ψ ∘ Z := hZ_meas.exists_eq_measurable_comp
  rw [h_eqY, h_eqZ]
  exact h_indep.comp hφ_meas hψ_meas

of_measurable_left🔗

LemmaProbabilityTheory.CondIndepFun.of_measurable_left
Details

No docstring.

🔗theorem
ProbabilityTheory.CondIndepFun.of_measurable_left.{u_1, u_2, u_3, u_4,
    u_5}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4}
  {γ' : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
  {mγ' : MeasurableSpace γ'} [StandardBorelSpace γ'] [Nonempty γ']
  {μ : MeasureTheory.Measure α} {X : α → β} {hX : Measurable X}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'} [StandardBorelSpace α]
  [MeasureTheory.IsFiniteMeasure μ]
  (h_indep :
    CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y Z μ)
  (hY_meas : Measurable Y') :
  CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y' Z μ
ProbabilityTheory.CondIndepFun.of_measurable_left.{u_1,
    u_2, u_3, u_4, u_5}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {δ : Type u_4}
  {γ' : Type u_5} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {mγ' : MeasurableSpace γ'}
  [StandardBorelSpace γ'] [Nonempty γ']
  {μ : MeasureTheory.Measure α}
  {X : α → β} {hX : Measurable X}
  {Y : α → γ} {Z : α → δ} {Y' : α → γ'}
  [StandardBorelSpace α]
  [MeasureTheory.IsFiniteMeasure μ]
  (h_indep :
    CondIndepFun
      (MeasurableSpace.comap X
        inferInstance)
      ⋯ Y Z μ)
  (hY_meas : Measurable Y') :
  CondIndepFun
    (MeasurableSpace.comap X
      inferInstance)
    ⋯ Y' Z μ

Code

lemma CondIndepFun.of_measurable_left
    (h_indep : Y ⟂ᵢ[X, hX; μ] Z) (hY_meas : Measurable[mγ.comap Y] Y') :
    Y' ⟂ᵢ[X, hX; μ] Z

Actions: Source · Open Issue

Proof
by
  obtain ⟨φ, hφ_meas, h_eqY⟩ : ∃ φ, Measurable φ ∧ Y' = φ ∘ Y := hY_meas.exists_eq_measurable_comp
  rw [h_eqY]
  exact h_indep.comp hφ_meas measurable_id

of_measurable_right🔗

LemmaProbabilityTheory.CondIndepFun.of_measurable_right
Details

No docstring.

🔗theorem
ProbabilityTheory.CondIndepFun.of_measurable_right.{u_1, u_2, u_3, u_4,
    u_6}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4}
  {δ' : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
  {mδ' : MeasurableSpace δ'} [StandardBorelSpace δ'] [Nonempty δ']
  {μ : MeasureTheory.Measure α} {X : α → β} {hX : Measurable X}
  {Y : α → γ} {Z : α → δ} {Z' : α → δ'} [StandardBorelSpace α]
  [MeasureTheory.IsFiniteMeasure μ]
  (h_indep :
    CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y Z μ)
  (hZ_meas : Measurable Z') :
  CondIndepFun (MeasurableSpace.comap X inferInstance) ⋯ Y Z' μ
ProbabilityTheory.CondIndepFun.of_measurable_right.{u_1,
    u_2, u_3, u_4, u_6}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {δ : Type u_4}
  {δ' : Type u_6} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  {mδ' : MeasurableSpace δ'}
  [StandardBorelSpace δ'] [Nonempty δ']
  {μ : MeasureTheory.Measure α}
  {X : α → β} {hX : Measurable X}
  {Y : α → γ} {Z : α → δ} {Z' : α → δ'}
  [StandardBorelSpace α]
  [MeasureTheory.IsFiniteMeasure μ]
  (h_indep :
    CondIndepFun
      (MeasurableSpace.comap X
        inferInstance)
      ⋯ Y Z μ)
  (hZ_meas : Measurable Z') :
  CondIndepFun
    (MeasurableSpace.comap X
      inferInstance)
    ⋯ Y Z' μ

Code

lemma CondIndepFun.of_measurable_right
    (h_indep : Y ⟂ᵢ[X, hX; μ] Z) (hZ_meas : Measurable[mδ.comap Z] Z') :
    Y ⟂ᵢ[X, hX; μ] Z'
Used by (1)

Actions: Source · Open Issue

Proof
by
  obtain ⟨ψ, hψ_meas, h_eqZ⟩ : ∃ ψ, Measurable ψ ∧ Z' = ψ ∘ Z := hZ_meas.exists_eq_measurable_comp
  rw [h_eqZ]
  exact h_indep.comp measurable_id hψ_meas
  1. ProbabilityTheory.Kernel.IndepFun.of_prod_right
  2. ProbabilityTheory.Kernel.IndepFun.of_prod_left
  3. ProbabilityTheory.CondIndepFun.of_prod_right
  4. ProbabilityTheory.CondIndepFun.of_prod_left
  5. ProbabilityTheory.IndepFun.of_measurable
  6. ProbabilityTheory.IndepFun.of_measurable_left
  7. ProbabilityTheory.IndepFun.of_measurable_right
  8. ProbabilityTheory.CondIndepFun.of_measurable
  9. ProbabilityTheory.CondIndepFun.of_measurable_left
  10. ProbabilityTheory.CondIndepFun.of_measurable_right