Lower Lebesgue integral for ℝ≥0∞-valued functions

We define the lower Lebesgue integral of an ℝ≥0∞-valued function.

Notation

We introduce the following notation for the lower Lebesgue integral of a function f : α → ℝ≥0∞.

• ∫⁻ x, f x ∂μ: integral of a function f : α → ℝ≥0∞ with respect to a measure μ;
• ∫⁻ x, f x: integral of a function f : α → ℝ≥0∞ with respect to the canonical measure volume on α;
• ∫⁻ x in s, f x ∂μ: integral of a function f : α → ℝ≥0∞ over a set s with respect to a measure μ, defined as ∫⁻ x, f x ∂(μ.restrict s);
• ∫⁻ x in s, f x: integral of a function f : α → ℝ≥0∞ over a set s with respect to the canonical measure volume, defined as ∫⁻ x, f x ∂(volume.restrict s).

theorem MeasureTheory.lintegral_def {α : Type u_5} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) : MeasureTheory.lintegral μ f = ⨆ (g : MeasureTheory.SimpleFunc α ENNReal), ⨆ (_ : ⇑g ≤ f), g.lintegral μ

@[irreducible]

def MeasureTheory.lintegral {α : Type u_5} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) : ENNReal

The lower Lebesgue integral of a function f with respect to a measure μ.

Equations

• MeasureTheory.lintegral μ f = ⨆ (g : MeasureTheory.SimpleFunc α ENNReal), ⨆ (_ : ⇑g ≤ f), g.lintegral μ

In the notation for integrals, an expression like ∫⁻ x, g ‖x‖ ∂μ will not be parsed correctly, and needs parentheses. We do not set the binding power of r to 0, because then ∫⁻ x, f x = 0 will be parsed incorrectly.

def MeasureTheory.«term∫⁻_,_∂_» : Lean.ParserDescr

The lower Lebesgue integral of a function f with respect to a measure μ.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∫⁻_,_∂_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∫⁻_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∫⁻_,_» : Lean.ParserDescr

The lower Lebesgue integral of a function f with respect to a measure μ.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∫⁻_In_,_∂_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∫⁻_In_,_∂_» : Lean.ParserDescr

The lower Lebesgue integral of a function f with respect to a measure μ.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∫⁻_In_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∫⁻_In_,_» : Lean.ParserDescr

The lower Lebesgue integral of a function f with respect to a measure μ.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.SimpleFunc.lintegral_eq_lintegral {α : Type u_1} {m : MeasurableSpace α} (f : MeasureTheory.SimpleFunc α ENNReal) (μ : MeasureTheory.Measure α) : ∫⁻ (a : α), f a ∂μ = f.lintegral μ

theorem MeasureTheory.lintegral_mono' {α : Type u_1} {m : MeasurableSpace α} ⦃μ ν : MeasureTheory.Measure α⦄ (hμν : μ ≤ ν) ⦃f g : α → ENNReal⦄ (hfg : f ≤ g) : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν

theorem MeasureTheory.lintegral_mono_fn' {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} ⦃f g : α → ENNReal⦄ (hfg : ∀ (x : α), f x ≤ g x) (h2 : μ ≤ ν) : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν

theorem MeasureTheory.lintegral_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} ⦃f g : α → ENNReal⦄ (hfg : f ≤ g) : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_mono_fn {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} ⦃f g : α → ENNReal⦄ (hfg : ∀ (x : α), f x ≤ g x) : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_mono_nnreal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → NNReal} (h : f ≤ g) : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ∫⁻ (a : α), ↑(g a) ∂μ

theorem MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) : ⨆ (g : α → ENNReal), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_mono_set {α : Type u_1} {x✝ : MeasurableSpace α} ⦃μ : MeasureTheory.Measure α⦄ {s t : Set α} {f : α → ENNReal} (hst : s ⊆ t) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ

theorem MeasureTheory.lintegral_mono_set' {α : Type u_1} {x✝ : MeasurableSpace α} ⦃μ : MeasureTheory.Measure α⦄ {s t : Set α} {f : α → ENNReal} (hst : s ≤ᵐ[μ] t) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ

theorem MeasureTheory.monotone_lintegral {α : Type u_1} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Monotone (MeasureTheory.lintegral μ)

@[simp]

theorem MeasureTheory.lintegral_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) : ∫⁻ (x : α), c ∂μ = c * μ Set.univ

theorem MeasureTheory.lintegral_zero {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} : ∫⁻ (x : α), 0 ∂μ = 0

theorem MeasureTheory.lintegral_zero_fun {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.lintegral μ 0 = 0

theorem MeasureTheory.lintegral_one {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} : ∫⁻ (x : α), 1 ∂μ = μ Set.univ

theorem MeasureTheory.setLIntegral_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (c : ENNReal) : ∫⁻ (x : α) in s, c ∂μ = c * μ s

@[deprecated MeasureTheory.setLIntegral_const]

theorem MeasureTheory.set_lintegral_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (c : ENNReal) : ∫⁻ (x : α) in s, c ∂μ = c * μ s

Alias of MeasureTheory.setLIntegral_const.

theorem MeasureTheory.setLIntegral_one {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) : ∫⁻ (x : α) in s, 1 ∂μ = μ s

@[deprecated MeasureTheory.setLIntegral_one]

theorem MeasureTheory.set_lintegral_one {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) : ∫⁻ (x : α) in s, 1 ∂μ = μ s

Alias of MeasureTheory.setLIntegral_one.

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

@[deprecated MeasureTheory.setLIntegral_const_lt_top]

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

Alias of MeasureTheory.setLIntegral_const_lt_top.

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

theorem MeasureTheory.exists_measurable_le_lintegral_eq {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) : ∃ (g : α → ENNReal), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

For any function f : α → ℝ≥0∞, there exists a measurable function g ≤ f with the same integral.

theorem MeasureTheory.lintegral_eq_nnreal {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal) (μ : MeasureTheory.Measure α) : ∫⁻ (a : α), f a ∂μ = ⨆ (φ : MeasureTheory.SimpleFunc α NNReal), ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ

∫⁻ a in s, f a ∂μ is defined as the supremum of integrals of simple functions φ : α →ₛ ℝ≥0∞ such that φ ≤ f. This lemma says that it suffices to take functions φ : α →ₛ ℝ≥0.

theorem MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (h : ∫⁻ (x : α), f x ∂μ ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (φ : MeasureTheory.SimpleFunc α NNReal), (∀ (x : α), ↑(φ x) ≤ f x) ∧ ∀ (ψ : MeasureTheory.SimpleFunc α NNReal), (∀ (x : α), ↑(ψ x) ≤ f x) → (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal (ψ - φ)).lintegral μ < ε

theorem MeasureTheory.iSup_lintegral_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_5} (f : ι → α → ENNReal) : ⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), ⨆ (i : ι), f i a ∂μ

theorem MeasureTheory.iSup₂_lintegral_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_5} {ι' : ι → Sort u_6} (f : (i : ι) → ι' i → α → ENNReal) : ⨆ (i : ι), ⨆ (j : ι' i), ∫⁻ (a : α), f i j a ∂μ ≤ ∫⁻ (a : α), ⨆ (i : ι), ⨆ (j : ι' i), f i j a ∂μ

theorem MeasureTheory.le_iInf_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_5} (f : ι → α → ENNReal) : ∫⁻ (a : α), ⨅ (i : ι), f i a ∂μ ≤ ⨅ (i : ι), ∫⁻ (a : α), f i a ∂μ

theorem MeasureTheory.le_iInf₂_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_5} {ι' : ι → Sort u_6} (f : (i : ι) → ι' i → α → ENNReal) : ∫⁻ (a : α), ⨅ (i : ι), ⨅ (h : ι' i), f i h a ∂μ ≤ ⨅ (i : ι), ⨅ (h : ι' i), ∫⁻ (a : α), f i h a ∂μ

theorem MeasureTheory.lintegral_mono_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (h : ∀ᵐ (a : α) ∂μ, f a ≤ g a) : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.setLIntegral_mono_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal} (hg : AEMeasurable g (μ.restrict s)) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Lebesgue integral over a set is monotone in function.

This version assumes that the upper estimate is an a.e. measurable function and the estimate holds a.e. on the set. See also setLIntegral_mono_ae' for a version that assumes measurability of the set but assumes no regularity of either function.

@[deprecated MeasureTheory.setLIntegral_mono_ae]

theorem MeasureTheory.set_lintegral_mono_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal} (hg : AEMeasurable g (μ.restrict s)) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Alias of MeasureTheory.setLIntegral_mono_ae.

---

Lebesgue integral over a set is monotone in function.

This version assumes that the upper estimate is an a.e. measurable function and the estimate holds a.e. on the set. See also setLIntegral_mono_ae' for a version that assumes measurability of the set but assumes no regularity of either function.

theorem MeasureTheory.setLIntegral_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal} (hg : Measurable g) (hfg : ∀ x ∈ s, f x ≤ g x) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

@[deprecated MeasureTheory.setLIntegral_mono]

theorem MeasureTheory.set_lintegral_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal} (hg : Measurable g) (hfg : ∀ x ∈ s, f x ≤ g x) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Alias of MeasureTheory.setLIntegral_mono.

theorem MeasureTheory.setLIntegral_mono_ae' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal} (hs : MeasurableSet s) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

@[deprecated MeasureTheory.setLIntegral_mono_ae']

theorem MeasureTheory.set_lintegral_mono_ae' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal} (hs : MeasurableSet s) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Alias of MeasureTheory.setLIntegral_mono_ae'.

theorem MeasureTheory.setLIntegral_mono' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal} (hs : MeasurableSet s) (hfg : ∀ x ∈ s, f x ≤ g x) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

@[deprecated MeasureTheory.setLIntegral_mono']

theorem MeasureTheory.set_lintegral_mono' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal} (hs : MeasurableSet s) (hfg : ∀ x ∈ s, f x ≤ g x) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Alias of MeasureTheory.setLIntegral_mono'.

theorem MeasureTheory.setLIntegral_le_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (f : α → ENNReal) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ

@[deprecated MeasureTheory.setLIntegral_le_lintegral]

theorem MeasureTheory.set_lintegral_le_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (f : α → ENNReal) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ

Alias of MeasureTheory.setLIntegral_le_lintegral.

theorem MeasureTheory.lintegral_congr_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (h : f =ᵐ[μ] g) : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_congr {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (h : ∀ (a : α), f a = g a) : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.setLIntegral_congr {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s t : Set α} (h : s =ᵐ[μ] t) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

@[deprecated MeasureTheory.setLIntegral_congr]

theorem MeasureTheory.set_lintegral_congr {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s t : Set α} (h : s =ᵐ[μ] t) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

Alias of MeasureTheory.setLIntegral_congr.

theorem MeasureTheory.setLIntegral_congr_fun {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} {s : Set α} (hs : MeasurableSet s) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

@[deprecated MeasureTheory.setLIntegral_congr_fun]

theorem MeasureTheory.set_lintegral_congr_fun {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} {s : Set α} (hs : MeasurableSet s) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Alias of MeasureTheory.setLIntegral_congr_fun.

theorem MeasureTheory.lintegral_ofReal_le_lintegral_nnnorm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ℝ) : ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ↑‖f x‖₊ ∂μ

theorem MeasureTheory.lintegral_nnnorm_eq_of_ae_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (h_nonneg : 0 ≤ᵐ[μ] f) : ∫⁻ (x : α), ↑‖f x‖₊ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

theorem MeasureTheory.lintegral_nnnorm_eq_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (h_nonneg : 0 ≤ f) : ∫⁻ (x : α), ↑‖f x‖₊ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

theorem MeasureTheory.lintegral_iSup {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) (h_mono : Monotone f) : ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Monotone convergence theorem -- sometimes called Beppo-Levi convergence. See lintegral_iSup_directed for a more general form.

theorem MeasureTheory.lintegral_iSup' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ℕ) => f n x) : ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Monotone convergence theorem -- sometimes called Beppo-Levi convergence. Version with ae_measurable functions.

theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ℕ) => f n x) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (F x))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))

Monotone convergence theorem expressed with limits

theorem MeasureTheory.lintegral_eq_iSup_eapprox_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f a ∂μ = ⨆ (n : ℕ), (MeasureTheory.SimpleFunc.eapprox f n).lintegral μ

theorem MeasureTheory.exists_pos_setLIntegral_lt_of_measure_lt {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (h : ∫⁻ (x : α), f x ∂μ ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

If f has finite integral, then ∫⁻ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero. This lemma states this fact in terms of ε and δ.

@[deprecated MeasureTheory.exists_pos_setLIntegral_lt_of_measure_lt]

theorem MeasureTheory.exists_pos_set_lintegral_lt_of_measure_lt {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (h : ∫⁻ (x : α), f x ∂μ ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

Alias of MeasureTheory.exists_pos_setLIntegral_lt_of_measure_lt.

---

If f has finite integral, then ∫⁻ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero. This lemma states this fact in terms of ε and δ.

theorem MeasureTheory.tendsto_setLIntegral_zero {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5} {f : α → ENNReal} (h : ∫⁻ (x : α), f x ∂μ ≠ ⊤) {l : Filter ι} {s : ι → Set α} (hl : Filter.Tendsto (⇑μ ∘ s) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α) in s i, f x ∂μ) l (nhds 0)

If f has finite integral, then ∫⁻ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero.

@[deprecated MeasureTheory.tendsto_setLIntegral_zero]

theorem MeasureTheory.tendsto_set_lintegral_zero {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5} {f : α → ENNReal} (h : ∫⁻ (x : α), f x ∂μ ≠ ⊤) {l : Filter ι} {s : ι → Set α} (hl : Filter.Tendsto (⇑μ ∘ s) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α) in s i, f x ∂μ) l (nhds 0)

Alias of MeasureTheory.tendsto_setLIntegral_zero.

---

If f has finite integral, then ∫⁻ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero.

theorem MeasureTheory.le_lintegral_add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : α → ENNReal) : ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a + g a ∂μ

The sum of the lower Lebesgue integrals of two functions is less than or equal to the integral of their sum. The other inequality needs one of these functions to be (a.e.-)measurable.

theorem MeasureTheory.lintegral_add_aux {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hf : Measurable f) (hg : Measurable g) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

@[simp]

theorem MeasureTheory.lintegral_add_left {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) (g : α → ENNReal) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

If f g : α → ℝ≥0∞ are two functions and one of them is (a.e.) measurable, then the Lebesgue integral of f + g equals the sum of integrals. This lemma assumes that f is integrable, see also MeasureTheory.lintegral_add_right and primed versions of these lemmas.

theorem MeasureTheory.lintegral_add_left' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (g : α → ENNReal) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_add_right' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {g : α → ENNReal} (hg : AEMeasurable g μ) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

@[simp]

theorem MeasureTheory.lintegral_add_right {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {g : α → ENNReal} (hg : Measurable g) : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

If f g : α → ℝ≥0∞ are two functions and one of them is (a.e.) measurable, then the Lebesgue integral of f + g equals the sum of integrals. This lemma assumes that g is integrable, see also MeasureTheory.lintegral_add_left and primed versions of these lemmas.

@[simp]

theorem MeasureTheory.lintegral_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) (f : α → ENNReal) : ∫⁻ (a : α), f a ∂c • μ = c * ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.setLIntegral_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) (f : α → ENNReal) (s : Set α) : ∫⁻ (a : α) in s, f a ∂c • μ = c * ∫⁻ (a : α) in s, f a ∂μ

@[deprecated MeasureTheory.setLIntegral_smul_measure]

theorem MeasureTheory.set_lintegral_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) (f : α → ENNReal) (s : Set α) : ∫⁻ (a : α) in s, f a ∂c • μ = c * ∫⁻ (a : α) in s, f a ∂μ

Alias of MeasureTheory.setLIntegral_smul_measure.

@[simp]

theorem MeasureTheory.lintegral_zero_measure {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal) : ∫⁻ (a : α), f a ∂0 = 0

@[simp]

theorem MeasureTheory.lintegral_add_measure {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal) (μ ν : MeasureTheory.Measure α) : ∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), f a ∂ν

@[simp]

theorem MeasureTheory.lintegral_finset_sum_measure {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (s : Finset ι) (f : α → ENNReal) (μ : ι → MeasureTheory.Measure α) : ∫⁻ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫⁻ (a : α), f a ∂μ i

@[simp]

theorem MeasureTheory.lintegral_sum_measure {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (f : α → ENNReal) (μ : ι → MeasureTheory.Measure α) : ∫⁻ (a : α), f a ∂MeasureTheory.Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i

theorem MeasureTheory.hasSum_lintegral_measure {α : Type u_1} {ι : Type u_5} {x✝ : MeasurableSpace α} (f : α → ENNReal) (μ : ι → MeasureTheory.Measure α) : HasSum (fun (i : ι) => ∫⁻ (a : α), f a ∂μ i) (∫⁻ (a : α), f a ∂MeasureTheory.Measure.sum μ)

@[simp]

theorem MeasureTheory.lintegral_of_isEmpty {α : Type u_5} [MeasurableSpace α] [IsEmpty α] (μ : MeasureTheory.Measure α) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = 0

theorem MeasureTheory.setLIntegral_empty {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) : ∫⁻ (x : α) in ∅, f x ∂μ = 0

@[deprecated MeasureTheory.setLIntegral_empty]

theorem MeasureTheory.set_lintegral_empty {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) : ∫⁻ (x : α) in ∅, f x ∂μ = 0

Alias of MeasureTheory.setLIntegral_empty.

theorem MeasureTheory.setLIntegral_univ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) : ∫⁻ (x : α) in Set.univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

@[deprecated MeasureTheory.setLIntegral_univ]

theorem MeasureTheory.set_lintegral_univ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) : ∫⁻ (x : α) in Set.univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Alias of MeasureTheory.setLIntegral_univ.

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

@[deprecated MeasureTheory.setLIntegral_measure_zero]

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

Alias of MeasureTheory.setLIntegral_measure_zero.

theorem MeasureTheory.lintegral_finset_sum' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β) {f : β → α → ENNReal} (hf : ∀ b ∈ s, AEMeasurable (f b) μ) : ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

theorem MeasureTheory.lintegral_finset_sum {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β) {f : β → α → ENNReal} (hf : ∀ b ∈ s, Measurable (f b)) : ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

@[simp]

theorem MeasureTheory.lintegral_const_mul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_const_mul'' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal} (hf : AEMeasurable f μ) : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_const_mul_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal) : r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ

theorem MeasureTheory.lintegral_const_mul' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal) (hr : r ≠ ⊤) : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_mul_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

theorem MeasureTheory.lintegral_mul_const'' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal} (hf : AEMeasurable f μ) : ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

theorem MeasureTheory.lintegral_mul_const_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal) : (∫⁻ (a : α), f a ∂μ) * r ≤ ∫⁻ (a : α), f a * r ∂μ

theorem MeasureTheory.lintegral_mul_const' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal) (hr : r ≠ ⊤) : ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

theorem MeasureTheory.lintegral_lintegral_mul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → ENNReal} {g : β → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) : ∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

theorem MeasureTheory.lintegral_rw₁ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f f' : α → β} (h : f =ᵐ[μ] f') (g : β → ENNReal) : ∫⁻ (a : α), g (f a) ∂μ = ∫⁻ (a : α), g (f' a) ∂μ

theorem MeasureTheory.lintegral_rw₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f₁ f₁' : α → β} {f₂ f₂' : α → γ} (h₁ : f₁ =ᵐ[μ] f₁') (h₂ : f₂ =ᵐ[μ] f₂') (g : β → γ → ENNReal) : ∫⁻ (a : α), g (f₁ a) (f₂ a) ∂μ = ∫⁻ (a : α), g (f₁' a) (f₂' a) ∂μ

theorem MeasureTheory.lintegral_indicator_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) (s : Set α) : ∫⁻ (a : α), s.indicator f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ

@[simp]

theorem MeasureTheory.lintegral_indicator {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ENNReal) : ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

theorem MeasureTheory.setLIntegral_indicator {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (hs : MeasurableSet s) (f : α → ENNReal) : ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ

theorem MeasureTheory.lintegral_indicator₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (f : α → ENNReal) : ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

theorem MeasureTheory.setLIntegral_indicator₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s t : Set α} (hs : MeasureTheory.NullMeasurableSet s (μ.restrict t)) : ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ

theorem MeasureTheory.lintegral_indicator_const_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (c : ENNReal) : ∫⁻ (a : α), s.indicator (fun (x : α) => c) a ∂μ ≤ c * μ s

theorem MeasureTheory.lintegral_indicator_const₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (c : ENNReal) : ∫⁻ (a : α), s.indicator (fun (x : α) => c) a ∂μ = c * μ s

theorem MeasureTheory.lintegral_indicator_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (c : ENNReal) : ∫⁻ (a : α), s.indicator (fun (x : α) => c) a ∂μ = c * μ s

theorem MeasureTheory.setLIntegral_eq_of_support_subset {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal} (hsf : Function.support f ⊆ s) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂μ

theorem MeasureTheory.setLIntegral_eq_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) (r : ENNReal) : ∫⁻ (x : α) in {x : α | f x = r}, f x ∂μ = r * μ {x : α | f x = r}

@[deprecated MeasureTheory.setLIntegral_eq_const]

theorem MeasureTheory.set_lintegral_eq_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) (r : ENNReal) : ∫⁻ (x : α) in {x : α | f x = r}, f x ∂μ = r * μ {x : α | f x = r}

Alias of MeasureTheory.setLIntegral_eq_const.

theorem MeasureTheory.lintegral_indicator_one_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) : ∫⁻ (a : α), s.indicator 1 a ∂μ ≤ μ s

@[simp]

theorem MeasureTheory.lintegral_indicator_one₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : ∫⁻ (a : α), s.indicator 1 a ∂μ = μ s

@[simp]

theorem MeasureTheory.lintegral_indicator_one {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : ∫⁻ (a : α), s.indicator 1 a ∂μ = μ s

theorem MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hle : f ≤ᵐ[μ] g) (hg : AEMeasurable g μ) (ε : ENNReal) : ∫⁻ (a : α), f a ∂μ + ε * μ {x : α | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ

A version of Markov's inequality for two functions. It doesn't follow from the standard Markov's inequality because we only assume measurability of g, not f.

theorem MeasureTheory.mul_meas_ge_le_lintegral₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (ε : ENNReal) : ε * μ {x : α | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

Markov's inequality also known as Chebyshev's first inequality.

theorem MeasureTheory.mul_meas_ge_le_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) (ε : ENNReal) : ε * μ {x : α | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

Markov's inequality also known as Chebyshev's first inequality. For a version assuming AEMeasurable, see mul_meas_ge_le_lintegral₀.

theorem MeasureTheory.meas_le_lintegral₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {s : Set α} (hs : ∀ x ∈ s, 1 ≤ f x) : μ s ≤ ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_le_meas {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal} (hf : ∀ (a : α), f a ≤ 1) (h'f : ∀ a ∈ sᶜ, f a = 0) : ∫⁻ (a : α), f a ∂μ ≤ μ s

theorem MeasureTheory.setLIntegral_le_meas {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (hs : MeasurableSet s) {f : α → ENNReal} (hf : ∀ a ∈ s, a ∈ t → f a ≤ 1) (hf' : ∀ a ∈ s, a ∉ t → f a = 0) : ∫⁻ (a : α) in s, f a ∂μ ≤ μ t

theorem MeasureTheory.lintegral_eq_top_of_measure_eq_top_ne_zero {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (hμf : μ {x : α | f x = ⊤} ≠ 0) : ∫⁻ (x : α), f x ∂μ = ⊤

theorem MeasureTheory.setLintegral_eq_top_of_measure_eq_top_ne_zero {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α} (hf : AEMeasurable f (μ.restrict s)) (hμf : μ {x : α | x ∈ s ∧ f x = ⊤} ≠ 0) : ∫⁻ (x : α) in s, f x ∂μ = ⊤

theorem MeasureTheory.measure_eq_top_of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (hμf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : μ {x : α | f x = ⊤} = 0

theorem MeasureTheory.measure_eq_top_of_setLintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α} (hf : AEMeasurable f (μ.restrict s)) (hμf : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤) : μ {x : α | x ∈ s ∧ f x = ⊤} = 0

theorem MeasureTheory.meas_ge_le_lintegral_div {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {ε : ENNReal} (hε : ε ≠ 0) (hε' : ε ≠ ⊤) : μ {x : α | ε ≤ f x} ≤ (∫⁻ (a : α), f a ∂μ) / ε

Markov's inequality, also known as Chebyshev's first inequality.

theorem MeasureTheory.ae_eq_of_ae_le_of_lintegral_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hfg : f ≤ᵐ[μ] g) (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (hg : AEMeasurable g μ) (hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ) : f =ᵐ[μ] g

@[simp]

theorem MeasureTheory.lintegral_eq_zero_iff' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) : ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᵐ[μ] 0

@[simp]

theorem MeasureTheory.lintegral_eq_zero_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᵐ[μ] 0

theorem MeasureTheory.setLIntegral_eq_zero_iff' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) {f : α → ENNReal} (hf : AEMeasurable f (μ.restrict s)) : ∫⁻ (a : α) in s, f a ∂μ = 0 ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0

theorem MeasureTheory.setLIntegral_eq_zero_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α) in s, f a ∂μ = 0 ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0

theorem MeasureTheory.lintegral_pos_iff_support {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) : 0 < ∫⁻ (a : α), f a ∂μ ↔ 0 < μ (Function.support f)

theorem MeasureTheory.setLintegral_pos_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) {s : Set α} : 0 < ∫⁻ (a : α) in s, f a ∂μ ↔ 0 < μ (Function.support f ∩ s)

theorem MeasureTheory.lintegral_iSup_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) (h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a) : ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Weaker version of the monotone convergence theorem

theorem MeasureTheory.lintegral_sub' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hg : AEMeasurable g μ) (hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) (h_le : g ≤ᵐ[μ] f) : ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_sub {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hg : Measurable g) (hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) (h_le : g ≤ᵐ[μ] f) : ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_sub_le' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : α → ENNReal) (hf : AEMeasurable f μ) : ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ

theorem MeasureTheory.lintegral_sub_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : α → ENNReal) (hf : Measurable f) : ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ

theorem MeasureTheory.lintegral_strict_mono_of_ae_le_of_frequently_ae_lt {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h_le : f ≤ᵐ[μ] g) (h : ∃ᵐ (x : α) ∂μ, f x ≠ g x) : ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

theorem MeasureTheory.lintegral_strict_mono_of_ae_le_of_ae_lt_on {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h_le : f ≤ᵐ[μ] g) {s : Set α} (hμs : μ s ≠ 0) (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x) : ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

theorem MeasureTheory.lintegral_strict_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hμ : μ ≠ 0) (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h : ∀ᵐ (x : α) ∂μ, f x < g x) : ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

theorem MeasureTheory.setLIntegral_strict_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} {s : Set α} (hsm : MeasurableSet s) (hs : μ s ≠ 0) (hg : Measurable g) (hfi : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤) (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x) : ∫⁻ (x : α) in s, f x ∂μ < ∫⁻ (x : α) in s, g x ∂μ

@[deprecated MeasureTheory.setLIntegral_strict_mono]

theorem MeasureTheory.set_lintegral_strict_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} {s : Set α} (hsm : MeasurableSet s) (hs : μ s ≠ 0) (hg : Measurable g) (hfi : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤) (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x) : ∫⁻ (x : α) in s, f x ∂μ < ∫⁻ (x : α) in s, g x ∂μ

Alias of MeasureTheory.setLIntegral_strict_mono.

theorem MeasureTheory.lintegral_iInf_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), Measurable (f n)) (h_mono : ∀ (n : ℕ), f n.succ ≤ᵐ[μ] f n) (h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Monotone convergence theorem for nonincreasing sequences of functions

theorem MeasureTheory.lintegral_iInf {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), Measurable (f n)) (h_anti : Antitone f) (h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Monotone convergence theorem for nonincreasing sequences of functions

theorem MeasureTheory.lintegral_iInf' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun (i : ℕ) => f i a) (h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

theorem MeasureTheory.lintegral_iInf_directed_of_measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [Countable β] {f : β → α → ENNReal} {μ : MeasureTheory.Measure α} (hμ : μ ≠ 0) (hf : ∀ (b : β), Measurable (f b)) (hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤) (h_directed : Directed (fun (x1 x2 : α → ENNReal) => x1 ≥ x2) f) : ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ

Monotone convergence for an infimum over a directed family and indexed by a countable type

theorem MeasureTheory.lintegral_liminf_le' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ) : ∫⁻ (a : α), Filter.liminf (fun (n : ℕ) => f n a) Filter.atTop ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop

Known as Fatou's lemma, version with AEMeasurable functions

theorem MeasureTheory.lintegral_liminf_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), Measurable (f n)) : ∫⁻ (a : α), Filter.liminf (fun (n : ℕ) => f n a) Filter.atTop ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop

Known as Fatou's lemma

theorem MeasureTheory.limsup_lintegral_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (g : α → ENNReal) (hf_meas : ∀ (n : ℕ), Measurable (f n)) (h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g) (h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) : Filter.limsup (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop ≤ ∫⁻ (a : α), Filter.limsup (fun (n : ℕ) => f n a) Filter.atTop ∂μ

theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ (n : ℕ), Measurable (F n)) (h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))

Dominated convergence theorem for nonnegative functions

theorem MeasureTheory.tendsto_lintegral_of_dominated_convergence' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ) (h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))

Dominated convergence theorem for nonnegative functions which are just almost everywhere measurable.

theorem MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ι) => F n a) l (nhds (f a))) : Filter.Tendsto (fun (n : ι) => ∫⁻ (a : α), F n a ∂μ) l (nhds (∫⁻ (a : α), f a ∂μ))

Dominated convergence theorem for filters with a countable basis

theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_antitone {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun (n : ℕ) => f n x) (h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (F x))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))

theorem MeasureTheory.lintegral_iSup_directed_of_measurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] {f : β → α → ENNReal} (hf : ∀ (b : β), Measurable (f b)) (h_directed : Directed (fun (x1 x2 : α → ENNReal) => x1 ≤ x2) f) : ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Monotone convergence for a supremum over a directed family and indexed by a countable type

theorem MeasureTheory.lintegral_iSup_directed {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] {f : β → α → ENNReal} (hf : ∀ (b : β), AEMeasurable (f b) μ) (h_directed : Directed (fun (x1 x2 : α → ENNReal) => x1 ≤ x2) f) : ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

Monotone convergence for a supremum over a directed family and indexed by a countable type.

theorem MeasureTheory.lintegral_tsum {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] {f : β → α → ENNReal} (hf : ∀ (i : β), AEMeasurable (f i) μ) : ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ

theorem MeasureTheory.lintegral_iUnion₀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] {s : β → Set α} (hm : ∀ (i : β), MeasureTheory.NullMeasurableSet (s i) μ) (hd : Pairwise (MeasureTheory.AEDisjoint μ on s)) (f : α → ENNReal) : ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

theorem MeasureTheory.lintegral_iUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] {s : β → Set α} (hm : ∀ (i : β), MeasurableSet (s i)) (hd : Pairwise (Disjoint on s)) (f : α → ENNReal) : ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

theorem MeasureTheory.lintegral_biUnion₀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set β} {s : β → Set α} (ht : t.Countable) (hm : ∀ i ∈ t, MeasureTheory.NullMeasurableSet (s i) μ) (hd : t.Pairwise (MeasureTheory.AEDisjoint μ on s)) (f : α → ENNReal) : ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ

theorem MeasureTheory.lintegral_biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set β} {s : β → Set α} (ht : t.Countable) (hm : ∀ i ∈ t, MeasurableSet (s i)) (hd : t.PairwiseDisjoint s) (f : α → ENNReal) : ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ

theorem MeasureTheory.lintegral_biUnion_finset₀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset β} {t : β → Set α} (hd : (↑s).Pairwise (MeasureTheory.AEDisjoint μ on t)) (hm : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (t b) μ) (f : α → ENNReal) : ∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ

theorem MeasureTheory.lintegral_biUnion_finset {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset β} {t : β → Set α} (hd : (↑s).PairwiseDisjoint t) (hm : ∀ b ∈ s, MeasurableSet (t b)) (f : α → ENNReal) : ∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ

theorem MeasureTheory.lintegral_iUnion_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] (s : β → Set α) (f : α → ENNReal) : ∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

theorem MeasureTheory.lintegral_union {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {A B : Set α} (hB : MeasurableSet B) (hAB : Disjoint A B) : ∫⁻ (a : α) in A ∪ B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ

theorem MeasureTheory.lintegral_union_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) (s t : Set α) : ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in t, f a ∂μ

theorem MeasureTheory.lintegral_inter_add_diff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {B : Set α} (f : α → ENNReal) (A : Set α) (hB : MeasurableSet B) : ∫⁻ (x : α) in A ∩ B, f x ∂μ + ∫⁻ (x : α) in A \ B, f x ∂μ = ∫⁻ (x : α) in A, f x ∂μ

theorem MeasureTheory.lintegral_add_compl {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {A : Set α} (hA : MeasurableSet A) : ∫⁻ (x : α) in A, f x ∂μ + ∫⁻ (x : α) in Aᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

theorem MeasureTheory.setLintegral_compl {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α} (hsm : MeasurableSet s) (hfs : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤) : ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ

theorem MeasureTheory.setLIntegral_iUnion_of_directed {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5} [Countable ι] (f : α → ENNReal) {s : ι → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) : ∫⁻ (x : α) in ⋃ (i : ι), s i, f x ∂μ = ⨆ (i : ι), ∫⁻ (x : α) in s i, f x ∂μ

theorem MeasureTheory.lintegral_max {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hf : Measurable f) (hg : Measurable g) : ∫⁻ (x : α), f x ⊔ g x ∂μ = ∫⁻ (x : α) in {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x : α | g x < f x}, f x ∂μ

theorem MeasureTheory.setLIntegral_max {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hf : Measurable f) (hg : Measurable g) (s : Set α) : ∫⁻ (x : α) in s, f x ⊔ g x ∂μ = ∫⁻ (x : α) in s ∩ {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in s ∩ {x : α | g x < f x}, f x ∂μ

@[deprecated MeasureTheory.setLIntegral_max]

theorem MeasureTheory.set_lintegral_max {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hf : Measurable f) (hg : Measurable g) (s : Set α) : ∫⁻ (x : α) in s, f x ⊔ g x ∂μ = ∫⁻ (x : α) in s ∩ {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in s ∩ {x : α | g x < f x}, f x ∂μ

Alias of MeasureTheory.setLIntegral_max.

theorem MeasureTheory.lintegral_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} (hf : Measurable f) (hg : Measurable g) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ

theorem MeasureTheory.lintegral_map' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} (hf : AEMeasurable f (MeasureTheory.Measure.map g μ)) (hg : AEMeasurable g μ) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ

theorem MeasureTheory.lintegral_map_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} (f : β → ENNReal) {g : α → β} (hg : Measurable g) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

theorem MeasureTheory.lintegral_comp {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace β] {f : β → ENNReal} {g : α → β} (hf : Measurable f) (hg : Measurable g) : MeasureTheory.lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ

theorem MeasureTheory.setLIntegral_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace β] {f : β → ENNReal} {g : α → β} {s : Set β} (hs : MeasurableSet s) (hf : Measurable f) (hg : Measurable g) : ∫⁻ (y : β) in s, f y ∂MeasureTheory.Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ

@[deprecated MeasureTheory.setLIntegral_map]

theorem MeasureTheory.set_lintegral_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace β] {f : β → ENNReal} {g : α → β} {s : Set β} (hs : MeasurableSet s) (hf : Measurable f) (hg : Measurable g) : ∫⁻ (y : β) in s, f y ∂MeasureTheory.Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ

Alias of MeasureTheory.setLIntegral_map.

theorem MeasureTheory.lintegral_indicator_const_comp {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {f : α → β} {s : Set β} (hf : Measurable f) (hs : MeasurableSet s) (c : ENNReal) : ∫⁻ (a : α), s.indicator (fun (x : β) => c) (f a) ∂μ = c * μ (f ⁻¹' s)

theorem MeasurableEmbedding.lintegral_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace β] {g : α → β} (hg : MeasurableEmbedding g) (f : β → ENNReal) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ

If g : α → β is a measurable embedding and f : β → ℝ≥0∞ is any function (not necessarily measurable), then ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ. Compare with lintegral_map which applies to any measurable g : α → β but requires that f is measurable as well.

theorem MeasureTheory.lintegral_map_equiv {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace β] (f : β → ENNReal) (g : α ≃ᵐ β) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map (⇑g) μ = ∫⁻ (a : α), f (g a) ∂μ

The lintegral transforms appropriately under a measurable equivalence g : α ≃ᵐ β. (Compare lintegral_map, which applies to a wider class of functions g : α → β, but requires measurability of the function being integrated.)

theorem MeasureTheory.MeasurePreserving.lintegral_map_equiv {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace β] {ν : MeasureTheory.Measure β} (f : β → ENNReal) (g : α ≃ᵐ β) (hg : MeasureTheory.MeasurePreserving (⇑g) μ ν) : ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f (g a) ∂μ

theorem MeasureTheory.MeasurePreserving.lintegral_comp {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mb : MeasurableSpace β} {ν : MeasureTheory.Measure β} {g : α → β} (hg : MeasureTheory.MeasurePreserving g μ ν) {f : β → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν

theorem MeasureTheory.MeasurePreserving.lintegral_comp_emb {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mb : MeasurableSpace β} {ν : MeasureTheory.Measure β} {g : α → β} (hg : MeasureTheory.MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ENNReal) : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν

theorem MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mb : MeasurableSpace β} {ν : MeasureTheory.Measure β} {g : α → β} (hg : MeasureTheory.MeasurePreserving g μ ν) {s : Set β} (hs : MeasurableSet s) {f : β → ENNReal} (hf : Measurable f) : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

@[deprecated MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage]

theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_preimage {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mb : MeasurableSpace β} {ν : MeasureTheory.Measure β} {g : α → β} (hg : MeasureTheory.MeasurePreserving g μ ν) {s : Set β} (hs : MeasurableSet s) {f : β → ENNReal} (hf : Measurable f) : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

Alias of MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage.

theorem MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mb : MeasurableSpace β} {ν : MeasureTheory.Measure β} {g : α → β} (hg : MeasureTheory.MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ENNReal) (s : Set β) : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

@[deprecated MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb]

theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_preimage_emb {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mb : MeasurableSpace β} {ν : MeasureTheory.Measure β} {g : α → β} (hg : MeasureTheory.MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ENNReal) (s : Set β) : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

Alias of MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb.

theorem MeasureTheory.MeasurePreserving.setLIntegral_comp_emb {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mb : MeasurableSpace β} {ν : MeasureTheory.Measure β} {g : α → β} (hg : MeasureTheory.MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ENNReal) (s : Set α) : ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν

@[deprecated MeasureTheory.MeasurePreserving.setLIntegral_comp_emb]

theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_emb {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mb : MeasurableSpace β} {ν : MeasureTheory.Measure β} {g : α → β} (hg : MeasureTheory.MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ENNReal) (s : Set α) : ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν

Alias of MeasureTheory.MeasurePreserving.setLIntegral_comp_emb.

theorem MeasureTheory.lintegral_subtype_comap {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ENNReal) : ∫⁻ (x : ↑s), f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫⁻ (x : α) in s, f x ∂μ

theorem MeasureTheory.setLIntegral_subtype {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (t : Set ↑s) (f : α → ENNReal) : ∫⁻ (x : ↑s) in t, f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ

theorem MeasureTheory.exists_setLintegral_compl_lt {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (s : Set α), MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

If f : α → ℝ≥0∞ has finite integral, then there exists a measurable set s of finite measure such that the integral of f over sᶜ is less than a given positive number.

Also used to prove an Lᵖ-norm version in MeasureTheory.Memℒp.exists_eLpNorm_indicator_compl_le.

theorem MeasureTheory.exists_measurable_le_setLintegral_eq_of_integrable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤) : ∃ (g : α → ENNReal), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

For any function f : α → ℝ≥0∞, there exists a measurable function g ≤ f with the same integral over any measurable set.

@[deprecated MeasureTheory.setLIntegral_subtype]

theorem MeasureTheory.set_lintegral_subtype {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (t : Set ↑s) (f : α → ENNReal) : ∫⁻ (x : ↑s) in t, f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ

Alias of MeasureTheory.setLIntegral_subtype.

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

theorem MeasureTheory.lintegral_dirac {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (f : α → ENNReal) : ∫⁻ (a : α), f a ∂MeasureTheory.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 ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0

@[deprecated MeasureTheory.setLIntegral_dirac']

theorem MeasureTheory.set_lintegral_dirac' {α : Type u_1} [MeasurableSpace α] {a : α} {f : α → ENNReal} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s) [Decidable (a ∈ s)] : ∫⁻ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0

Alias of MeasureTheory.setLIntegral_dirac'.

theorem MeasureTheory.setLIntegral_dirac {α : Type u_1} [MeasurableSpace α] {a : α} (f : α → ENNReal) (s : Set α) [MeasurableSingletonClass α] [Decidable (a ∈ s)] : ∫⁻ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0

@[deprecated MeasureTheory.setLIntegral_dirac]

theorem MeasureTheory.set_lintegral_dirac {α : Type u_1} [MeasurableSpace α] {a : α} (f : α → ENNReal) (s : Set α) [MeasurableSingletonClass α] [Decidable (a ∈ s)] : ∫⁻ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0

Alias of MeasureTheory.setLIntegral_dirac.

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

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

theorem ENNReal.tsum_const_eq {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (c : ENNReal) : ∑' (x : α), c = c * MeasureTheory.Measure.count Set.univ

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 counting measure with hypothesis using tsum in ℝ≥0.

Lebesgue integral over finite and countable types and sets

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

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

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

theorem MeasureTheory.lintegral_countable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.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} {m : MeasurableSpace α} {μ : MeasureTheory.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} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] (s : Finset α) (f : α → ENNReal) : ∫⁻ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, f x * μ {x}

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

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

theorem MeasureTheory.ae_lt_top' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : ∀ᵐ (x : α) ∂μ, f x < ⊤

theorem MeasureTheory.ae_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) (h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : ∀ᵐ (x : α) ∂μ, f x < ⊤

theorem MeasureTheory.setLIntegral_lt_top_of_le_nnreal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : μ s ≠ ⊤) {f : α → ENNReal} (hbdd : ∃ (y : NNReal), ∀ x ∈ s, f x ≤ ↑y) : ∫⁻ (x : α) in s, f x ∂μ < ⊤

Lebesgue integral of a bounded function over a set of finite measure is finite. Note that this lemma assumes no regularity of either f or s.

theorem MeasureTheory.setLIntegral_lt_top_of_bddAbove {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : μ s ≠ ⊤) {f : α → NNReal} (hbdd : BddAbove (f '' s)) : ∫⁻ (x : α) in s, ↑(f x) ∂μ < ⊤

Lebesgue integral of a bounded function over a set of finite measure is finite. Note that this lemma assumes no regularity of either f or s.

@[deprecated MeasureTheory.setLIntegral_lt_top_of_bddAbove]

theorem MeasureTheory.set_lintegral_lt_top_of_bddAbove {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : μ s ≠ ⊤) {f : α → NNReal} (hbdd : BddAbove (f '' s)) : ∫⁻ (x : α) in s, ↑(f x) ∂μ < ⊤

Alias of MeasureTheory.setLIntegral_lt_top_of_bddAbove.

---

Lebesgue integral of a bounded function over a set of finite measure is finite. Note that this lemma assumes no regularity of either f or s.

theorem MeasureTheory.setLIntegral_lt_top_of_isCompact {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] {s : Set α} (hs : μ s ≠ ⊤) (hsc : IsCompact s) {f : α → NNReal} (hf : Continuous f) : ∫⁻ (x : α) in s, ↑(f x) ∂μ < ⊤

@[deprecated MeasureTheory.setLIntegral_lt_top_of_isCompact]

theorem MeasureTheory.set_lintegral_lt_top_of_isCompact {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] {s : Set α} (hs : μ s ≠ ⊤) (hsc : IsCompact s) {f : α → NNReal} (hf : Continuous f) : ∫⁻ (x : α) in s, ↑(f x) ∂μ < ⊤

Alias of MeasureTheory.setLIntegral_lt_top_of_isCompact.

theorem IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal {α : Type u_5} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [μ_fin : MeasureTheory.IsFiniteMeasure μ] {f : α → ENNReal} (f_bdd : ∃ (c : NNReal), ∀ (x : α), f x ≤ ↑c) : ∫⁻ (x : α), f x ∂μ < ⊤

theorem MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone_aux {α : Type u_5} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : MeasureTheory.Measure α} (hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ) (hF_meas : AEMeasurable F μ) (hf_tendsto : Filter.Tendsto (fun (i : ℕ) => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun (i : ℕ) => f i a) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a) (h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f i a) Filter.atTop (nhds (F a))

If a monotone sequence of functions has an upper bound and the sequence of integrals of these functions tends to the integral of the upper bound, then the sequence of functions converges almost everywhere to the upper bound. Auxiliary version assuming moreover that the functions in the sequence are ae measurable.

theorem MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone {α : Type u_5} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : MeasureTheory.Measure α} (hF_meas : AEMeasurable F μ) (hf_tendsto : Filter.Tendsto (fun (i : ℕ) => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun (i : ℕ) => f i a) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a) (h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f i a) Filter.atTop (nhds (F a))

If a monotone sequence of functions has an upper bound and the sequence of integrals of these functions tends to the integral of the upper bound, then the sequence of functions converges almost everywhere to the upper bound.

theorem MeasureTheory.tendsto_of_lintegral_tendsto_of_antitone {α : Type u_5} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : MeasureTheory.Measure α} (hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ) (hf_tendsto : Filter.Tendsto (fun (i : ℕ) => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun (i : ℕ) => f i a) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a) (h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f i a) Filter.atTop (nhds (F a))

If an antitone sequence of functions has a lower bound and the sequence of integrals of these functions tends to the integral of the lower bound, then the sequence of functions converges almost everywhere to the lower bound.

theorem MeasureTheory.exists_measurable_le_forall_setLIntegral_eq {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.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} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.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.lintegral_trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.lintegral_trim_ae {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal} (hf : AEMeasurable f (μ.trim hm)) : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ

theorem MeasureTheory.univ_le_of_forall_fin_meas_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.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 α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.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.

@[deprecated MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le]

theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le' {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.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_of_measurable {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.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 α] {μ : MeasureTheory.Measure α} [MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : MeasureTheory.SimpleFunc α NNReal} {L : ENNReal} (hL : L < ∫⁻ (x : α), ↑(f x) ∂μ) : ∃ (g : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → NNReal} {L : ENNReal} (hL : L < ∫⁻ (x : α), ↑(f x) ∂μ) : ∃ (g : MeasureTheory.SimpleFunc α NNReal), (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

theorem MeasureTheory.tendsto_measure_of_ae_tendsto_indicator {α : Type u_5} [MeasurableSpace α] {A : Set α} {ι : Type u_6} (L : Filter ι) [L.IsCountablyGenerated] {As : ι → Set α} {μ : MeasureTheory.Measure α} (A_mble : MeasurableSet A) (As_mble : ∀ (i : ι), MeasurableSet (As i)) {B : Set α} (B_mble : MeasurableSet B) (B_finmeas : μ B ≠ ⊤) (As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B) (h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) : Filter.Tendsto (fun (i : ι) => μ (As i)) L (nhds (μ A))

If the indicators of measurable sets Aᵢ tend pointwise almost everywhere to the indicator of a measurable set A and we eventually have Aᵢ ⊆ B for some set B of finite measure, then the measures of Aᵢ tend to the measure of A.

theorem MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure {α : Type u_5} [MeasurableSpace α] {A : Set α} {ι : Type u_6} (L : Filter ι) [L.IsCountablyGenerated] {As : ι → Set α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (A_mble : MeasurableSet A) (As_mble : ∀ (i : ι), MeasurableSet (As i)) (h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) : Filter.Tendsto (fun (i : ι) => μ (As i)) L (nhds (μ A))

If μ is a finite measure and the indicators of measurable sets Aᵢ tend pointwise almost everywhere to the indicator of a measurable set A, then the measures μ Aᵢ tend to the measure μ A.