Theorem 8.7 — the trigonometric functions and $\pi$

Proved

Rudin.ch08_trigonometric_pi

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

analysis

$\cos(\pi/2) = 0$ and $\cos$ is positive on $[0, \pi/2)$ , so $\pi/2$ is the smallest positive zero of the cosine; the complex exponential has period $2\pi i$ ; and every complex number of modulus one is $e^{it}$ for a unique $t \in [0, 2\pi)$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch08_fourier

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.7: the number `π` is characterized by `cos (π/2) = 0` with `cos` positive
on `[0, π/2)`; the complex exponential has period `2πi`, and `e^{iθ}` parametrizes the unit
circle. -/
theorem ch08_trigonometric_pi :
    Real.cos (Real.pi / 2) = 0 ∧
    (∀ x ∈ Set.Ico (0 : ℝ) (Real.pi / 2), 0 < Real.cos x) ∧
    (∀ z : ℂ, Complex.exp (z + 2 * Real.pi * Complex.I) = Complex.exp z) ∧
    (∀ z : ℂ, ‖z‖ = 1 → ∃ t ∈ Set.Ico (0 : ℝ) (2 * Real.pi),
      z = Complex.exp (t * Complex.I)) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8, p. 183, Theorem 8.7

Read-back

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

Four unconditional assertions, combined into one statement, about $\pi$ and the exponential/trigonometric functions:

$\cos(\pi/2) = 0$ .
For every $x$ with $0 \le x < \pi/2$ : $\cos x > 0$ . (The left endpoint is included, the right excluded.)
For every $z \in \mathbb{C}$ : $\exp(z + 2\pi i) = \exp(z)$ — periodicity with period $2\pi i$ .
For every $z \in \mathbb{C}$ with $\lVert z\rVert = 1$ there exists a real $t$ with $0 \le t < 2\pi$ and $z = \exp(it)$ — every unit complex number is on the curve, with parameter in the half-open interval.

Nothing is asserted about uniqueness of $t$ in 4, about $\pi$ being the least positive zero of $\cos$ beyond what 1 and 2 say, or about $\sin$ .

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 8.7 — the trigonometric functions and π\piπ

Theorem 8.7 — the trigonometric functions and $\pi$