theorem MeasureTheory.triangle_inequality_integral {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : α → F) : ‖∫ (x : α), f x ∂μ‖ ≤ ∫ (x : α), ‖f x‖ ∂μ

Triangle inequality for integrals. For an integrable function $f : \alpha \to F$ taking values in a normed space, the norm of the integral is bounded by the integral of the norm: $\left\|\int f\, d\mu\right\| \le \int \|f\|\, d\mu$.

theorem MeasureTheory.integral_properties {α : Type u_1} [MeasurableSpace α] {μ : Measure α} : (∀ (f : α → ℝ), Integrable f μ → ‖∫ (x : α), f x ∂μ‖ ≤ ∫ (x : α), ‖f x‖ ∂μ) ∧ (∀ (f g : α → ℝ), Integrable g μ → f =ᶠ[ae μ] g → Integrable f μ ∧ ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ) ∧ ∀ (f g : α → ℝ), Integrable f μ → Integrable g μ → f ≤ᶠ[ae μ] g → ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ

Basic properties of the Lebesgue integral on $\mathbb{R}$. This combines three fundamental statements for measurable real-valued functions $f, g : \alpha \to \mathbb{R}$: (1) if $f$ is integrable, then $\left|\int f\right| \le \int |f|$; (2) if $g$ is integrable and $f = g$ almost everywhere, then $f$ is integrable and $\int f = \int g$; (3) if $f, g$ are integrable and $f \le g$ almost everywhere, then $\int f \le \int g$.

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

Additivity of the Lebesgue integral on $L^+$. For measurable functions $f, g : \alpha \to [0, \infty]$, the Lebesgue integral is additive: $\int (f + g)\, d\mu = \int f\, d\mu + \int g\, d\mu$.

theorem MeasureTheory.monotone_convergence_lintegral {α : Type u_1} [MeasurableSpace α] {μ : 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 (supremum form). If $\{f_n\}$ is a sequence of nonnegative measurable functions in $L^+(E)$ with $f_1 \le f_2 \le \cdots$ pointwise, then the integral of the pointwise supremum equals the supremum of the integrals: $\int \sup_n f_n\, d\mu = \sup_n \int f_n\, d\mu$.

theorem MeasureTheory.monotone_convergence_lintegral_tendsto {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : ℕ → α → ENNReal} {g : α → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) (h_mono : Monotone f) (h_lim : ∀ (a : α), Filter.Tendsto (fun (n : ℕ) => f n a) Filter.atTop (nhds (g a))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (a : α), f n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), g a ∂μ))

Monotone Convergence Theorem (limit form). If $\{f_n\}$ is a sequence of nonnegative measurable functions in $L^+(E)$ with $f_1 \le f_2 \le \cdots$ pointwise, and $f_n \to g$ pointwise everywhere, then $\lim_{n \to \infty} \int f_n\, d\mu = \int g\, d\mu$.

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

Fatou's lemma. For a sequence $\{f_n\}$ of nonnegative measurable functions in $L^+(E)$, the integral of the pointwise $\liminf$ is bounded by the $\liminf$ of the integrals: $\int \liminf_{n \to \infty} f_n\, d\mu \le \liminf_{n \to \infty} \int f_n\, d\mu$.

theorem MeasureTheory.measure_setOf_eq_top_of_lintegral_lt_top {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) (hfint : ∫⁻ (x : α), f x ∂μ < ⊤) : μ {x : α | f x = ⊤} = 0

A function with finite integral is finite a.e. If $f \in L^+(E)$ and $\int_E f < \infty$, then $\{x \in E : f(x) = \infty\}$ has measure zero.

theorem MeasureTheory.riemann_lebesgue_agree {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ} (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) : IntegrableOn f (Set.Icc a b) volume ∧ IntervalIntegrable f volume a b ∧ ∫ (x : ℝ) in Set.Icc a b, f x = ∫ (x : ℝ) in a..b, f x

Riemann and Lebesgue integrals agree for continuous functions. For $f \in C([a, b])$ with $a < b$, the function $f$ is Lebesgue integrable on $[a, b]$, is interval integrable, and its Lebesgue integral $\int_{[a, b]} f$ coincides with the Riemann integral $\int_a^b f(x)\, dx$.

theorem MeasureTheory.dominated_convergence_theorem {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {F : ℕ → α → G} {f : α → G} {g : α → ℝ} (hF_meas : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ) (hg_integrable : Integrable g μ) (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ g a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a))) : Integrable f μ ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))

Dominated Convergence Theorem. Let $g : \alpha \to [0, \infty)$ be a nonnegative integrable function, and let $\{F_n\}$ be a sequence of measurable functions such that (1) $\|F_n\| \le g$ almost everywhere for all $n$ and (2) $F_n \to f$ pointwise almost everywhere on $\alpha$. Then $f$ is integrable and $\lim_{n \to \infty} \int F_n\, d\mu = \int f\, d\mu$.

theorem Integration.integral_eq_posPart_sub_negPart {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) : ∫ (x : α), f x ∂μ = ∫ (x : α), (f x)⁺ ∂μ - ∫ (x : α), (f x)⁻ ∂μ

The integral of a real function as the difference of positive and negative parts. For an integrable function $f : \alpha \to \mathbb{R}$, the Lebesgue integral decomposes as $\int f\, d\mu = \int f^+\, d\mu - \int f^-\, d\mu$, where $f^+ = \max(f, 0)$ and $f^- = \max(-f, 0)$.