LeanMachineLearning exposition

ProbabilityTheory.CondIndepFun.of_prod_left🔗

Minimal Lean file

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