case h
α : Type u_2
β : Type ?u.1758361
γ : Type ?u.1758364
δ : Type ?u.1758367
m✝ : MeasurableSpace α
μ✝ ν : Measure α
ι : Type u_1
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity (sum μ) f) s = ↑↑(sum fun n => withDensity (μ n) f) s
α : Type u_2
β : Type ?u.1758361
γ : Type ?u.1758364
δ : Type ?u.1758367
m✝ : MeasurableSpace α
μ✝ ν : Measure α
ι : Type u_1
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
⊢ withDensity (sum μ) f = sum fun n => withDensity (μ n) f
ext1 s hs
no goals
case h
α : Type u_2
β : Type ?u.1758361
γ : Type ?u.1758364
δ : Type ?u.1758367
m✝ : MeasurableSpace α
μ✝ ν : Measure α
ι : Type u_1
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity (sum μ) f) s = ↑↑(sum fun n => withDensity (μ n) f) s
simp_rw [sum_apply _ hs, withDensity_apply f hs, restrict_sum μ hs, lintegral_sum_measure]