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_4} {m : MeasurableSpace α} (μ : Measure α) (f : α → ENNReal) : lintegral μ f = ⨆ (g : SimpleFunc α ENNReal), ⨆ (_ : ⇑g ≤ f), g.lintegral μ

@[irreducible]

noncomputable def MeasureTheory.lintegral {α : Type u_4} {m : MeasurableSpace α} (μ : 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∫⁻_,_∂_».«delab_app.MeasureTheory.lintegral» : 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∫⁻_,_» : 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_app.MeasureTheory.lintegral» : 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_,_∂_».«delab_app.MeasureTheory.lintegral» : 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_app.MeasureTheory.lintegral» : 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 : SimpleFunc α ENNReal) (μ : Measure α) : ∫⁻ (a : α), f a ∂μ = f.lintegral μ

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

theorem MeasureTheory.lintegral_mono_fn' {α : Type u_1} {m : MeasurableSpace α} {μ ν : 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 α} {μ : Measure α} ⦃f g : α → ENNReal⦄ (hfg : f ≤ g) : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ

theorem MeasureTheory.lintegral_mono_fn {α : Type u_1} {m : MeasurableSpace α} {μ : 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 α} {μ : 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 α} {μ : 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 α} ⦃μ : 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 α} ⦃μ : Measure α⦄ {s t : Set α} {f : α → ENNReal} (hst : s ≤ᶠ[ae μ] t) : ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ

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

@[simp]

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

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

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

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

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

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

theorem MeasureTheory.exists_measurable_le_lintegral_eq {α : Type u_1} {m : MeasurableSpace α} (μ : 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) (μ : Measure α) : ∫⁻ (a : α), f a ∂μ = ⨆ (φ : SimpleFunc α NNReal), ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (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 α} {μ : Measure α} {f : α → ENNReal} (h : ∫⁻ (x : α), f x ∂μ ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (φ : SimpleFunc α NNReal), (∀ (x : α), ↑(φ x) ≤ f x) ∧ ∀ (ψ : SimpleFunc α NNReal), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ENNReal.ofNNReal (ψ - φ)).lintegral μ < ε

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

theorem MeasureTheory.iSup₂_lintegral_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ι : Sort u_4} {ι' : ι → Sort u_5} (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 α} {μ : Measure α} {ι : Sort u_4} (f : ι → α → ENNReal) : ∫⁻ (a : α), ⨅ (i : ι), f i a ∂μ ≤ ⨅ (i : ι), ∫⁻ (a : α), f i a ∂μ

theorem MeasureTheory.le_iInf₂_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ι : Sort u_4} {ι' : ι → Sort u_5} (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 α} {μ : 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 α} {μ : 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.

theorem MeasureTheory.setLIntegral_mono {α : Type u_1} {m : MeasurableSpace α} {μ : 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 ∂μ

theorem MeasureTheory.setLIntegral_mono_ae' {α : Type u_1} {m : MeasurableSpace α} {μ : 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 ∂μ

theorem MeasureTheory.setLIntegral_mono' {α : Type u_1} {m : MeasurableSpace α} {μ : 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 ∂μ

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

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

theorem MeasureTheory.lintegral_congr {α : Type u_1} {m : MeasurableSpace α} {μ : 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 α} {μ : Measure α} {f : α → ENNReal} {s t : Set α} (h : s =ᶠ[ae μ] t) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

theorem MeasureTheory.setLIntegral_congr_fun {α : Type u_1} {m : MeasurableSpace α} {μ : 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 ∂μ

@[simp]

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

The Lebesgue integral is zero iff the function is a.e. zero.

@[simp]

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

theorem MeasureTheory.setLIntegral_eq_zero_iff' {α : Type u_1} {m : MeasurableSpace α} {μ : 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 α} {μ : 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 α} {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) : 0 < ∫⁻ (a : α), f a ∂μ ↔ 0 < μ (Function.support f)

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

theorem MeasureTheory.exists_pos_setLIntegral_lt_of_measure_lt {α : Type u_1} {m : MeasurableSpace α} {μ : 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 δ.

theorem MeasureTheory.tendsto_setLIntegral_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ι : Type u_4} {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.

@[simp]

theorem MeasureTheory.lintegral_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {R : Type u_4} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (f : α → ENNReal) : ∫⁻ (a : α), f a ∂c • μ = c • ∫⁻ (a : α), f a ∂μ

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

@[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) (μ ν : Measure α) : ∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), f a ∂ν

@[simp]

theorem MeasureTheory.lintegral_finset_sum_measure {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_4} (s : Finset ι) (f : α → ENNReal) (μ : ι → 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_4} (f : α → ENNReal) (μ : ι → Measure α) : ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i

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

@[simp]

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

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

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

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

theorem MeasureTheory.lintegral_rw₁ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {f f' : α → β} (h : f =ᶠ[ae μ] 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 α} {μ : Measure α} {f₁ f₁' : α → β} {f₂ f₂' : α → γ} (h₁ : f₁ =ᶠ[ae μ] f₁') (h₂ : f₂ =ᶠ[ae μ] 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 α} {μ : 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 α} {μ : 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 α} {μ : 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 α} {μ : Measure α} {s : Set α} (hs : NullMeasurableSet s μ) (f : α → ENNReal) : ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

theorem MeasureTheory.setLIntegral_indicator₀ {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : α → ENNReal) {s t : Set α} (hs : 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 α} {μ : Measure α} (s : Set α) (c : ENNReal) : ∫⁻ (a : α), s.indicator (fun (x : α) => c) a ∂μ ≤ c * μ s

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

theorem MeasureTheory.lintegral_indicator_const {α : Type u_1} {m : MeasurableSpace α} {μ : 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 α} {μ : 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 α} {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) (r : ENNReal) : ∫⁻ (x : α) in {x : α | f x = r}, f x ∂μ = r * μ {x : α | f x = r}

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

@[simp]

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

@[simp]

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

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

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

theorem MeasureTheory.lintegral_iUnion₀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [Countable β] {s : β → Set α} (hm : ∀ (i : β), NullMeasurableSet (s i) μ) (hd : Pairwise (Function.onFun (AEDisjoint μ) 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 α} {μ : Measure α} [Countable β] {s : β → Set α} (hm : ∀ (i : β), MeasurableSet (s i)) (hd : Pairwise (Function.onFun Disjoint 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 α} {μ : Measure α} {t : Set β} {s : β → Set α} (ht : t.Countable) (hm : ∀ i ∈ t, NullMeasurableSet (s i) μ) (hd : t.Pairwise (Function.onFun (AEDisjoint μ) 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 α} {μ : 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 α} {μ : Measure α} {s : Finset β} {t : β → Set α} (hd : (↑s).Pairwise (Function.onFun (AEDisjoint μ) t)) (hm : ∀ b ∈ s, 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 α} {μ : 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 α} {μ : 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 α} {μ : 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 α} {μ : 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 α} {μ : 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 α} {μ : Measure α} (f : α → ENNReal) {A : Set α} (hA : MeasurableSet A) : ∫⁻ (x : α) in A, f x ∂μ + ∫⁻ (x : α) in Aᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

theorem MeasureTheory.lintegral_piecewise {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (f g : α → ENNReal) [(j : α) → Decidable (j ∈ s)] : ∫⁻ (a : α), s.piecewise f g a ∂μ = ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ

theorem MeasureTheory.setLintegral_compl {α : Type u_1} {m : MeasurableSpace α} {μ : 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 α} {μ : Measure α} {ι : Type u_4} [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 α} {μ : 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 α} {μ : 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 ∂μ

theorem MeasureTheory.setLIntegral_lt_top_of_le_nnreal {α : Type u_1} {m : MeasurableSpace α} {μ : 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 α} {μ : 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.

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