LeanMachineLearning exposition

ProbabilityTheory.Kernel.prodMkLeft_deterministic🔗

Minimal Lean file

prodMkLeft_deterministic🔗

LemmaProbabilityTheory.Kernel.prodMkLeft_deterministic
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.prodMkLeft_deterministic.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β}
  (hf : Measurable f) :
  prodMkLeft γ (deterministic f hf) =
    deterministic (fun p => f (Prod.snd p)) ⋯
ProbabilityTheory.Kernel.prodMkLeft_deterministic.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {f : α → β}
  (hf : Measurable f) :
  prodMkLeft γ (deterministic f hf) =
    deterministic
      (fun p => f (Prod.snd p)) ⋯

Code

lemma prodMkLeft_deterministic {f : α → β} (hf : Measurable f) :
    (Kernel.deterministic f hf).prodMkLeft γ =
      Kernel.deterministic (fun p ↦ f p.2) (by fun_prop)
Used by (1)

Actions: Source · Open Issue

Proof
by
  ext
  simp [Kernel.deterministic_apply]