case pos
α : Type u_1
β : Type ?u.32980
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : HaveLebesgueDecomposition μ ν
⊢ Measurable (rnDeriv μ ν)

case neg
α : Type u_1
β : Type ?u.32980
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : ¬HaveLebesgueDecomposition μ ν
⊢ Measurable (rnDeriv μ ν)
α : Type u_1
β : Type ?u.32980
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
⊢ Measurable (rnDeriv μ ν)
by_cases h : HaveLebesgueDecomposition μ ν
no goals
case pos
α : Type u_1
β : Type ?u.32980
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : HaveLebesgueDecomposition μ ν
⊢ Measurable (rnDeriv μ ν)
exact (haveLebesgueDecomposition_spec μ ν).1
case neg
α : Type u_1
β : Type ?u.32980
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : ¬HaveLebesgueDecomposition μ ν
⊢ Measurable 0
case neg
α : Type u_1
β : Type ?u.32980
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : ¬HaveLebesgueDecomposition μ ν
⊢ Measurable (rnDeriv μ ν)
rw [rnDeriv, dif_neg h]
no goals
case neg
α : Type u_1
β : Type ?u.32980
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : ¬HaveLebesgueDecomposition μ ν
⊢ Measurable 0
exact measurable_zero