α : Type u_1
β : Type ?u.60618
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑ν s < ⊤ → (∫⁻ (x : α) in s, f x ∂ν) = ∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν
α : Type u_1
β : Type ?u.60618
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
⊢ f =ᶠ[ae ν] rnDeriv μ ν
refine' ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite hf (measurable_rnDeriv μ ν) _
α : Type u_1
β : Type ?u.60618
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
a : Set α
ha : MeasurableSet a
a✝ : ↑↑ν a < ⊤
⊢ (∫⁻ (x : α) in a, f x ∂ν) = ∫⁻ (x : α) in a, rnDeriv μ ν x ∂ν
α : Type u_1
β : Type ?u.60618
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑ν s < ⊤ → (∫⁻ (x : α) in s, f x ∂ν) = ∫⁻ (x : α) in s, rnDeriv μ ν x ∂ν
intro a ha _
no goals
α : Type u_1
β : Type ?u.60618
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
a : Set α
ha : MeasurableSet a
a✝ : ↑↑ν a < ⊤
⊢ (∫⁻ (x : α) in a, f x ∂ν) = ∫⁻ (x : α) in a, rnDeriv μ ν x ∂ν
calc
  (∫⁻ x : α in a, f x ∂ν) = ν.withDensity f a := (withDensity_apply f ha).symm
  _ = ν.withDensity (μ.rnDeriv ν) a := by rw [eq_withDensity_rnDeriv hf hs hadd]
  _ = ∫⁻ x : α in a, μ.rnDeriv ν x ∂ν := withDensity_apply _ ha
no goals
α : Type u_1
β : Type ?u.60618
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
a : Set α
ha : MeasurableSet a
a✝ : ↑↑ν a < ⊤
⊢ ↑↑(withDensity ν f) a = ↑↑(withDensity ν (rnDeriv μ ν)) a
rw [eq_withDensity_rnDeriv hf hs hadd]