case hfm
α : Type u_1
β : Type ?u.2764
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ AEMeasurable fun x => rnDeriv μ ν x

case hf
α : Type u_1
β : Type ?u.2764
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂restrict ν i, rnDeriv μ ν x < ⊤
α : Type u_1
β : Type ?u.2764
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, ENNReal.toReal (rnDeriv μ ν x) ∂ν) = ENNReal.toReal (↑↑μ i)
rw [integral_toReal, ← withDensity_apply _ hi, withDensity_rnDeriv_eq μ ν h]
no goals
case hfm
α : Type u_1
β : Type ?u.2764
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ AEMeasurable fun x => rnDeriv μ ν x
measurability
case hf
α : Type u_1
β : Type ?u.2764
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α) in Set.univ, rnDeriv μ ν x ∂ν) < ⊤
case hf
α : Type u_1
β : Type ?u.2764
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂restrict ν i, rnDeriv μ ν x < ⊤
refine' ae_lt_top (μ.measurable_rnDeriv ν)
  (lt_of_le_of_lt (lintegral_mono_set i.subset_univ) _).ne
case hf
α : Type u_1
β : Type ?u.2764
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ ↑↑μ Set.univ < ⊤
case hf
α : Type u_1
β : Type ?u.2764
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α) in Set.univ, rnDeriv μ ν x ∂ν) < ⊤
rw [← withDensity_apply _ MeasurableSet.univ, withDensity_rnDeriv_eq μ ν h]
no goals
case hf
α : Type u_1
β : Type ?u.2764
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ ↑↑μ Set.univ < ⊤
exact measure_lt_top _ _