Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.Kernel.deleteRight_map_prod

PFR.Mathlib.Probability.Kernel.Composition.Comp · PFR/Mathlib/Probability/Kernel/Composition/Comp.lean:126 to 141

Mathematical statement

Exact Lean statement

@[simp, nolint simpNF]
lemma deleteRight_map_prod (κ : Kernel α β) {f : β → γ} {g : β → δ} {g' : β → ε}
    (hg' : Measurable g') :
    deleteRight (map κ (fun b ↦ (f b, g b, g' b)))
      = map κ (fun b ↦ (f b, g b))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp, nolint simpNF]lemma deleteRight_map_prod (κ : Kernel α β) {f : β → γ} {g : β → δ} {g' : β → ε}    (hg' : Measurable g') :    deleteRight (map κ (fun b ↦ (f b, g b, g' b)))      = map κ (fun b ↦ (f b, g b)) := by  by_cases hfg : Measurable (fun b ↦ (f b, g b))  · have : Measurable f := hfg.fst    have : Measurable g := hfg.snd    rw [deleteRight_eq, map_map _ (by fun_prop) (by fun_prop)]    rfl  · have : ¬ (Measurable (fun b ↦ (f b, g b, g' b))) := by      contrapose! hfg      have T : Measurable g := hfg.snd.fst      have U : Measurable f := hfg.fst      exact U.prod T    simp [map_of_not_measurable _ hfg, map_of_not_measurable _ this]