TODO

Rename setLIntegral_congr to setLIntegral_congr_set

theorem MeasureTheory.lintegral_eq_zero_of_ae_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal} (hs : μ sᶜ = 0) (hf : ∀ x ∈ s, f x = 0) (hmes : MeasurableSet s) : ∫⁻ (x : α), f x ∂μ = 0

theorem MeasureTheory.lintegral_eq_setLIntegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : μ sᶜ = 0) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ

theorem MeasureTheory.lintegral_piecewise {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ENNReal) (g : α → ENNReal) [(j : α) → Decidable (j ∈ s)] : ∫⁻ (a : α), s.piecewise f g a ∂μ = ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ

theorem MeasureTheory.lintegral_eq_sum {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) (f : α → ENNReal) [Fintype α] : ∫⁻ (x : α), f x ∂μ = ∑ x : α, μ {x} * f x

theorem MeasureTheory.lintegral_eq_tsum {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) (f : α → ENNReal) [Countable α] : ∫⁻ (x : α), f x ∂μ = ∑' (x : α), μ {x} * f x

theorem MeasureTheory.setLIntegral_eq_sum {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) (s : Finset α) (f : α → ENNReal) : ∫⁻ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, μ {x} * f x

theorem MeasureTheory.lintegral_eq_single {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) (a : α) (f : α → ENNReal) (ha : ∀ (b : α), b ≠ a → f b = 0) : ∫⁻ (x : α), f x ∂μ = f a * μ {a}