α : Type u_1
β : Type ?u.1727935
γ : Type ?u.1727938
δ : Type ?u.1727941
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ (∑' (i : α), ∫⁻ (a : α), f a ∂↑↑μ {i} • dirac i) = ∑' (a : α), f a * ↑↑μ {a}
α : Type u_1
β : Type ?u.1727935
γ : Type ?u.1727938
δ : Type ?u.1727941
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a ∂μ) = ∑' (a : α), f a * ↑↑μ {a}
conv_lhs => rw [← sum_smul_dirac μ, lintegral_sum_measure]
case e_f.h
α : Type u_1
β : Type ?u.1727935
γ : Type ?u.1727938
δ : Type ?u.1727941
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ (∫⁻ (a : α), f a ∂↑↑μ {a} • dirac a) = f a * ↑↑μ {a}
α : Type u_1
β : Type ?u.1727935
γ : Type ?u.1727938
δ : Type ?u.1727941
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ (∑' (i : α), ∫⁻ (a : α), f a ∂↑↑μ {i} • dirac i) = ∑' (a : α), f a * ↑↑μ {a}
congr 1 with a : 1
no goals
case e_f.h
α : Type u_1
β : Type ?u.1727935
γ : Type ?u.1727938
δ : Type ?u.1727941
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ (∫⁻ (a : α), f a ∂↑↑μ {a} • dirac a) = f a * ↑↑μ {a}
rw [lintegral_smul_measure, lintegral_dirac, mul_comm]