α : Type u_1
β : Type ?u.1763263
γ : Type ?u.1763266
δ : Type ?u.1763269
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : ↑↑μ s = 0
⊢ ↑↑(withDensity μ f) s = 0
α : Type u_1
β : Type ?u.1763263
γ : Type ?u.1763266
δ : Type ?u.1763269
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ withDensity μ f ≪ μ
refine' AbsolutelyContinuous.mk fun s hs₁ hs₂ => _
α : Type u_1
β : Type ?u.1763263
γ : Type ?u.1763266
δ : Type ?u.1763269
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : ↑↑μ s = 0
⊢ (∫⁻ (a : α) in s, f a ∂μ) = 0
α : Type u_1
β : Type ?u.1763263
γ : Type ?u.1763266
δ : Type ?u.1763269
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : ↑↑μ s = 0
⊢ ↑↑(withDensity μ f) s = 0
rw [withDensity_apply _ hs₁]
no goals
α : Type u_1
β : Type ?u.1763263
γ : Type ?u.1763266
δ : Type ?u.1763269
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : ↑↑μ s = 0
⊢ (∫⁻ (a : α) in s, f a ∂μ) = 0
exact set_lintegral_measure_zero _ _ hs₂