# Lebesgue integral over finite and countable types, sets and measures #

The lemmas in this file require at least one of the following of the Lebesgue integral:

- The type of the set of integration is finite or countable
- The set of integration is finite or countable
- The measure is finite, s-finite or sigma-finite

source
theorem MeasureTheory.setLIntegral_const_lt_top {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] (s : Set α) {c : ENNReal} (hc : c ≠ ⊤) :
∫⁻ (x : α) in s, c ∂μ < ⊤
source
theorem MeasureTheory.lintegral_const_lt_top {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] {c : ENNReal} (hc : c ≠ ⊤) :
∫⁻ (x : α), c ∂μ < ⊤
source
theorem MeasureTheory.lintegral_eq_const {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] {f : α → ENNReal} {c : ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x = c) :
∫⁻ (x : α), f x ∂μ = c
source
theorem MeasureTheory.lintegral_le_const {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] {f : α → ENNReal} {c : ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x ≤ c) :
∫⁻ (x : α), f x ∂μ ≤ c
source
theorem MeasureTheory.iInf_le_lintegral {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] (f : α → ENNReal) :
⨅ (x : α), f x ≤ ∫⁻ (x : α), f x ∂μ
source
theorem MeasureTheory.lintegral_le_iSup {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] (f : α → ENNReal) :
∫⁻ (x : α), f x ∂μ ≤ ⨆ (x : α), f x
source
theorem IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {f : α → ENNReal} (f_bdd : ∃ (c : NNReal), ∀ (x : α), f x ≤ ↑c) :
∫⁻ (x : α), f x ∂μ < ⊤
source
theorem MeasureTheory.lintegral_dirac' {α : Type u_1} [MeasurableSpace α] (a : α) {f : α → ENNReal} (hf : Measurable f) :
∫⁻ (a : α), f a ∂Measure.dirac a = f a
source
@[simp]
theorem MeasureTheory.lintegral_dirac {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (f : α → ENNReal) :
∫⁻ (a : α), f a ∂Measure.dirac a = f a
source
theorem MeasureTheory.setLIntegral_dirac' {α : Type u_1} [MeasurableSpace α] {a : α} {f : α → ENNReal} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s) [Decidable (a ∈ s)] :
∫⁻ (x : α) in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0
source
theorem MeasureTheory.setLIntegral_dirac {α : Type u_1} [MeasurableSpace α] {a : α} (f : α → ENNReal) (s : Set α) [MeasurableSingletonClass α] [Decidable (a ∈ s)] :
∫⁻ (x : α) in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0
source
theorem MeasureTheory.lintegral_count' {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) :
∫⁻ (a : α), f a ∂Measure.count = ∑' (a : α), f a
source
theorem MeasureTheory.lintegral_count {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (f : α → ENNReal) :
∫⁻ (a : α), f a ∂Measure.count = ∑' (a : α), f a
source
theorem ENNReal.count_const_le_le_of_tsum_le {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α → ENNReal} (a_mble : Measurable a) {c : ENNReal} (tsum_le_c : ∑' (i : α), a i ≤ c) {ε : ENNReal} (ε_ne_zero : ε ≠ 0) (ε_ne_top : ε ≠ ⊤) :
MeasureTheory.Measure.count {i : α | ε ≤ a i} ≤ c / ε

Markov's inequality for the counting measure with hypothesis using `tsum` in `ℝ≥0∞`.

source
theorem NNReal.count_const_le_le_of_tsum_le {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α → NNReal} (a_mble : Measurable a) (a_summable : Summable a) {c : NNReal} (tsum_le_c : ∑' (i : α), a i ≤ c) {ε : NNReal} (ε_ne_zero : ε ≠ 0) :
MeasureTheory.Measure.count {i : α | ε ≤ a i} ≤ ↑c / ↑ε

Markov's inequality for the counting measure with hypothesis using `tsum` in `ℝ≥0`.

source
theorem MeasureTheory.lintegral_countable' {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [Countable α] [MeasurableSingletonClass α] (f : α → ENNReal) :
∫⁻ (a : α), f a ∂μ = ∑' (a : α), f a * μ {a}
source
theorem MeasureTheory.lintegral_singleton' {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) (a : α) :
∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}
source
theorem MeasureTheory.lintegral_singleton {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [MeasurableSingletonClass α] (f : α → ENNReal) (a : α) :
∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}
source
theorem MeasureTheory.lintegral_countable {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [MeasurableSingletonClass α] (f : α → ENNReal) {s : Set α} (hs : s.Countable) :
∫⁻ (a : α) in s, f a ∂μ = ∑' (a : ↑s), f ↑a * μ {↑a}
source
theorem MeasureTheory.lintegral_insert {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [MeasurableSingletonClass α] {a : α} {s : Set α} (h : a ∉ s) (f : α → ENNReal) :
∫⁻ (x : α) in insert a s, f x ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ
source
theorem MeasureTheory.lintegral_finset {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [MeasurableSingletonClass α] (s : Finset α) (f : α → ENNReal) :
∫⁻ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, f x * μ {x}
source
theorem MeasureTheory.lintegral_fintype {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [MeasurableSingletonClass α] [Fintype α] (f : α → ENNReal) :
∫⁻ (x : α), f x ∂μ = ∑ x : α, f x * μ {x}
source
theorem MeasureTheory.lintegral_unique {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [Unique α] (f : α → ENNReal) :
∫⁻ (x : α), f x ∂μ = f default * μ Set.univ
source
theorem MeasureTheory.exists_measurable_le_forall_setLIntegral_eq {α : Type u_1} [MeasurableSpace α] (μ : Measure α) [SFinite μ] (f : α → ENNReal) :
∃ (g : α → ENNReal), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

If `μ` is an s-finite measure, then for any function `f` there exists a measurable function `g ≤ f` that has the same Lebesgue integral over every set.

For the integral over the whole space, the statement is true without extra assumptions, see `exists_measurable_le_lintegral_eq`. See also `MeasureTheory.Measure.restrict_toMeasurable_of_sFinite` for a similar result.

source
theorem MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite {α : Type u_1} [MeasurableSpace α] (μ : Measure α) [SigmaFinite μ] {ε : ENNReal} (ε0 : ε ≠ 0) :
∃ (g : α → NNReal), (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ε

In a sigma-finite measure space, there exists an integrable function which is positive everywhere (and with an arbitrarily small integral).

source
theorem MeasureTheory.univ_le_of_forall_fin_meas_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (C : ENNReal) {f : Set α → ENNReal} (hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C) (h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ (n : ℕ), S n) ≤ ⨆ (n : ℕ), f (S n)) :
f Set.univ ≤ C
source
theorem MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (C : ENNReal) {f : α → ENNReal} (hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) :
∫⁻ (x : α), f x ∂μ ≤ C

If the Lebesgue integral of a function is bounded by some constant on all sets with finite measure in a sub-σ-algebra and the measure is σ-finite on that sub-σ-algebra, then the integral over the whole space is bounded by that same constant.

source
theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le_of_measurable {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (C : ENNReal) {f : α → ENNReal} (hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) :
∫⁻ (x : α), f x ∂μ ≤ C

Alias of `MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le`.

If the Lebesgue integral of a function is bounded by some constant on all sets with finite measure in a sub-σ-algebra and the measure is σ-finite on that sub-σ-algebra, then the integral over the whole space is bounded by that same constant.

source
theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ] (C : ENNReal) {f : α → ENNReal} (hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) :
∫⁻ (x : α), f x ∂μ ≤ C

If the Lebesgue integral of a function is bounded by some constant on all sets with finite measure and the measure is σ-finite, then the integral over the whole space is bounded by that same constant.

source
theorem MeasureTheory.SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {f : SimpleFunc α NNReal} {L : ENNReal} (hL : L < ∫⁻ (x : α), ↑(f x) ∂μ) :
∃ (g : SimpleFunc α NNReal), (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
source
theorem MeasureTheory.exists_lt_lintegral_simpleFunc_of_lt_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {f : α → NNReal} {L : ENNReal} (hL : L < ∫⁻ (x : α), ↑(f x) ∂μ) :
∃ (g : SimpleFunc α NNReal), (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ