LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Imported Lean Pool material for LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable.

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

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

theorem MeasureTheory.setLIntegral_eq_sum {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : 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 α] (μ : Measure α) (a : α) (f : α → ENNReal) (ha : ∀ (b : α), b ≠ a → f b = 0) : ∫⁻ (x : α), f x ∂μ = f a * μ {a}