Theorems 11.26 and 11.27 — comparison and the triangle inequality

Proved

Rudin.ch11_integral_abs_le

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysismeasure-theory

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorems 11.26 and 11.27: if `f` is integrable then so is `|f|` and
`|∫ f| ≤ ∫ |f|`; and a measurable function dominated by an integrable function is
integrable. -/
theorem ch11_integral_abs_le {X : Type*} [MeasurableSpace X] (μ : Measure X) (f g : X → ℝ) :
    (Integrable f μ → Integrable (fun x => |f x|) μ ∧ |∫ x, f x ∂μ| ≤ ∫ x, |f x| ∂μ) ∧
    (Measurable f → Integrable g μ → (∀ x, |f x| ≤ g x) → Integrable f μ) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 11, pp. 317-318, Theorems 11.26 and 11.27

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $X$ be a measurable space with measure $\mu$ and let $f, g : X \to \mathbb{R}$ be arbitrary functions. Two independent implications are asserted together:

If $f$ is integrable with respect to $\mu$ , then $|f|$ is integrable and

\Bigl| \int_X f \,d\mu \Bigr| \;\le\; \int_X |f| \,d\mu .

If $f$ is measurable, $g$ is integrable, and $|f(x)| \le g(x)$ for every $x \in X$ (pointwise everywhere, not merely almost everywhere), then $f$ is integrable.

In part 2 the dominating function $g$ is not assumed nonnegative explicitly; that follows from the domination inequality. The two parts share the ambient data but neither uses the other's hypotheses.

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph