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

theorem MeasureTheory.setLIntegral_const_lt_top {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] (s : Set α) {c : ENNReal} (hc : c ≠ ⊤) : ∫⁻ (x : α) in s, c ∂μ < ⊤

theorem MeasureTheory.lintegral_const_lt_top {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] {c : ENNReal} (hc : c ≠ ⊤) : ∫⁻ (x : α), c ∂μ < ⊤

theorem MeasureTheory.lintegral_eq_const {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] {f : α → ENNReal} {c : ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x = c) : ∫⁻ (x : α), f x ∂μ = c

theorem MeasureTheory.lintegral_le_const {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] {f : α → ENNReal} {c : ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x ≤ c) : ∫⁻ (x : α), f x ∂μ ≤ c

theorem MeasureTheory.iInf_le_lintegral {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] (f : α → ENNReal) : ⨅ (x : α), f x ≤ ∫⁻ (x : α), f x ∂μ

theorem MeasureTheory.lintegral_le_iSup {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ ≤ ⨆ (x : α), f x

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 ∂μ < ⊤

theorem MeasureTheory.lintegral_dirac' {α : Type u_1} [MeasurableSpace α] (a : α) {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f a ∂Measure.dirac a = f a

@[simp]

theorem MeasureTheory.lintegral_dirac {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (f : α → ENNReal) : ∫⁻ (a : α), f a ∂Measure.dirac a = f a

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

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

theorem MeasureTheory.lintegral_count' {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f a ∂Measure.count = ∑' (a : α), f a

theorem MeasureTheory.lintegral_count {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (f : α → ENNReal) : ∫⁻ (a : α), f a ∂Measure.count = ∑' (a : α), f a

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∞.

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.

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

theorem MeasureTheory.lintegral_singleton' {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) (a : α) : ∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}

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

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}

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 ∂μ

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

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

theorem MeasureTheory.lintegral_unique {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [Unique α] (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = f default * μ Set.univ

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.

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).

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

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.

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.

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.

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) ∂μ

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) ∂μ