case pos
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : HaveLebesgueDecomposition μ ν
⊢ singularPart μ ν ≤ μ

case neg
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : ¬HaveLebesgueDecomposition μ ν
⊢ singularPart μ ν ≤ μ
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
⊢ singularPart μ ν ≤ μ
by_cases hl : HaveLebesgueDecomposition μ ν
case pos.intro
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : HaveLebesgueDecomposition μ ν
left✝ : singularPart μ ν ⟂ₘ ν
h : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ singularPart μ ν ≤ μ
case pos
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : HaveLebesgueDecomposition μ ν
⊢ singularPart μ ν ≤ μ
cases' (haveLebesgueDecomposition_spec μ ν).2 with _ h
case pos.intro
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : HaveLebesgueDecomposition μ ν
left✝ : singularPart μ ν ⟂ₘ ν
h : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ singularPart μ ν ≤ singularPart μ ν + withDensity ν (rnDeriv μ ν)
case pos.intro
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : HaveLebesgueDecomposition μ ν
left✝ : singularPart μ ν ⟂ₘ ν
h : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ singularPart μ ν ≤ μ
conv_rhs => rw [h]
no goals
case pos.intro
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : HaveLebesgueDecomposition μ ν
left✝ : singularPart μ ν ⟂ₘ ν
h : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ singularPart μ ν ≤ singularPart μ ν + withDensity ν (rnDeriv μ ν)
exact Measure.le_add_right le_rfl
case neg
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : ¬HaveLebesgueDecomposition μ ν
⊢ 0 ≤ μ
case neg
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : ¬HaveLebesgueDecomposition μ ν
⊢ singularPart μ ν ≤ μ
rw [singularPart, dif_neg hl]
no goals
case neg
α : Type u_1
β : Type ?u.33660
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
hl : ¬HaveLebesgueDecomposition μ ν
⊢ 0 ≤ μ
exact Measure.zero_le μ