LeanMachineLearning exposition

ProbabilityTheory.Kernel.IndepFun.of_prod_right🔗

Minimal Lean file

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