Existing in Mathlib · Analysis

Fréchet–Riesz Representation Theorem

Every continuous linear functional on a Hilbert space is evaluation against one unique vector by the inner product. The representing vector has the same norm as the functional, and complex scalar multiplication is conjugated on the vector side.

Hilbert spaces
continuous duals
inner products
conjugate linearity
isometric equivalence
orthogonal complements

Exact definition

Exact Mathlib definition

def InnerProductSpace.toDual (𝕜 E : Type*) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : E ≃ₗᵢ⋆[𝕜] StrongDual 𝕜 E

The theorem at a glance

Fréchet–Riesz representation at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

An ivory functional-analysis poster identifies each continuous linear functional with inner product against one vector and traces the kernel-orthogonal-complement proof route. — A Hilbert space and its continuous dual are conjugate-linearly isometrically equivalent.

Statement structure

From hypotheses to conclusion

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

A vector in a complete inner-product space sweeps an inner-product pairing across the space and becomes a norm-matched continuous functional in the dual. — Inner product with a unique vector represents every continuous linear functional on a Hilbert space.

Why it matters

A mathematical landmark

Fréchet–Riesz turns abstract continuous linear functionals into concrete vectors and makes a Hilbert space canonically self-dual up to conjugation. Mathlib records the full isometric equivalence, not only existence of representatives.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's constructed conjugate-linear isometric equivalence between a complete RCLike inner-product space and its continuous dual, sending x to the functional y ↦ inner 𝕜 x y. It does not represent arbitrary algebraic or unbounded functionals, apply to arbitrary Banach spaces, or state Riesz–Markov.

Proof Atlas did not originate the Fréchet–Riesz theorem or Mathlib's definition.
In the complex case the equivalence is conjugate-linear, not ordinary complex-linear, and completeness is material for surjectivity.
The generated explanation and visuals are not proof evidence.

Source and local evidence

Where the theorem comes from

Existing declaration: InnerProductSpace.toDual in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.frechet-riesz-representation-theorem.v001
Source: Open the pinned upstream reference