Theorem 11.35 — the Schwarz inequality in $\mathscr{L}^2$

Proved

Rudin.ch11_schwarz

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

analysismeasure-theory

If $f, g \in \mathscr{L}^2(\mu)$ then $fg$ is integrable and $\left|\int fg\,d\mu\right| \le \|f\|_2\,\|g\|_2$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 11.35 (Schwarz inequality in `ℒ²`): if `f, g ∈ ℒ²(μ)` then `f g` is
integrable and `|∫ f g dμ| ≤ ‖f‖₂ ‖g‖₂`. -/
theorem ch11_schwarz {X : Type*} [MeasurableSpace X] (μ : Measure X) (f g : X → ℝ)
    (hf : MemL2 μ f) (hg : MemL2 μ g) :
    Integrable (fun x => f x * g x) μ ∧
      |∫ x, f x * g x ∂μ| ≤ L2Norm μ f * L2Norm μ g := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 11, p. 326, Theorem 11.35

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}$ each belong to $\mathcal{L}^2(\mu)$ , meaning each is measurable and has integrable square. Then both:

the pointwise product $x \mapsto f(x)g(x)$ is integrable with respect to $\mu$ ;

\Bigl| \int_X f g \, d\mu \Bigr| \;\le\; \lVert f\rVert_2 \,\lVert g \rVert_2, \qquad \lVert h \rVert_2 = \sqrt{\int_X h^2 \, d\mu}.

The norms are the square roots of the integrals of the squares (real square root, so nonnegative); no almost-everywhere or equivalence-class considerations enter, the statement being about the functions themselves.

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

Theorem 11.35 — the Schwarz inequality in L2\mathscr{L}^2L2

Theorem 11.35 — the Schwarz inequality in $\mathscr{L}^2$