Documentation

PFR.Mathlib.MeasureTheory.Integral.Lebesgue

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