case pos
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl : HaveLebesgueDecomposition μ ν
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤

case neg
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl : ¬HaveLebesgueDecomposition μ ν
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤
by_cases hl : HaveLebesgueDecomposition μ ν
case pos
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤
case pos
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl : HaveLebesgueDecomposition μ ν
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤
haveI := hl
case pos.intro.intro
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤
case pos
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤
obtain ⟨-, -, hadd⟩ := haveLebesgueDecomposition_spec μ ν
case pos.intro.intro
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this✝ : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
this : (∫⁻ (x : α) in toMeasurable μ s, rnDeriv μ ν x ∂ν) < ⊤
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤

case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ (∫⁻ (x : α) in toMeasurable μ s, rnDeriv μ ν x ∂ν) < ⊤
case pos.intro.intro
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤
suffices : (∫⁻ x in toMeasurable μ s, μ.rnDeriv ν x ∂ν) < ∞
case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ (∫⁻ (x : α) in toMeasurable μ s, rnDeriv μ ν x ∂ν) < ⊤
case pos.intro.intro
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this✝ : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
this : (∫⁻ (x : α) in toMeasurable μ s, rnDeriv μ ν x ∂ν) < ⊤
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤

case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ (∫⁻ (x : α) in toMeasurable μ s, rnDeriv μ ν x ∂ν) < ⊤
exact lt_of_le_of_lt (lintegral_mono_set (subset_toMeasurable _ _)) this
case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ ↑↑(withDensity ν fun x => rnDeriv μ ν x) (toMeasurable μ s) < ⊤
case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ (∫⁻ (x : α) in toMeasurable μ s, rnDeriv μ ν x ∂ν) < ⊤
rw [← withDensity_apply _ (measurableSet_toMeasurable _ _)]
case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ ↑↑(singularPart μ ν) (toMeasurable μ s) + ↑↑(withDensity ν (rnDeriv μ ν)) (toMeasurable μ s) < ⊤
case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ ↑↑(withDensity ν fun x => rnDeriv μ ν x) (toMeasurable μ s) < ⊤
refine'
  lt_of_le_of_lt
    (le_add_left le_rfl :
      _ ≤ μ.singularPart ν (toMeasurable μ s) + ν.withDensity (μ.rnDeriv ν) (toMeasurable μ s))
    _
case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ ↑↑μ s < ⊤
case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ ↑↑(singularPart μ ν) (toMeasurable μ s) + ↑↑(withDensity ν (rnDeriv μ ν)) (toMeasurable μ s) < ⊤
rw [← Measure.add_apply, ← hadd, measure_toMeasurable]
no goals
case this
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl this : HaveLebesgueDecomposition μ ν
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ ↑↑μ s < ⊤
exact hs.lt_top
case neg
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl : ¬HaveLebesgueDecomposition μ ν
⊢ 0 < ⊤
case neg
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl : ¬HaveLebesgueDecomposition μ ν
⊢ (∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν) < ⊤
erw [Measure.rnDeriv, dif_neg hl, lintegral_zero]
no goals
case neg
α : Type u_1
β : Type ?u.36188
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
s : Set α
hs : ↑↑μ s ≠ ⊤
hl : ¬HaveLebesgueDecomposition μ ν
⊢ 0 < ⊤
exact WithTop.zero_lt_top