LeanMachineLearning exposition

ProbabilityTheory.Kernel.IndepFun.of_prod_left🔗

Minimal Lean file

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