LeanMachineLearning exposition

ProbabilityTheory.Kernel.prodMkRight_deterministic🔗

Minimal Lean file

prodMkRight_deterministic🔗

LemmaProbabilityTheory.Kernel.prodMkRight_deterministic
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.prodMkRight_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) :
  prodMkRight γ (deterministic f hf) =
    deterministic (fun p => f (Prod.fst p)) ⋯
ProbabilityTheory.Kernel.prodMkRight_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) :
  prodMkRight γ (deterministic f hf) =
    deterministic
      (fun p => f (Prod.fst p)) ⋯

Code

lemma prodMkRight_deterministic {f : α → β} (hf : Measurable f) :
    (Kernel.deterministic f hf).prodMkRight γ =
      Kernel.deterministic (fun p ↦ f p.1) (by fun_prop)

Actions: Source · Open Issue

Proof
by
  ext
  simp [Kernel.deterministic_apply]