AcceptedTheorem · Statement with omitted proof

Riesz representation of bounded linear functionals

Every bounded linear functional on a Hilbert space has a unique representing vector of the same norm.

Larsson & Thomée ↗
Theorem A.1 · printed p. 228

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Every bounded linear functional on a Hilbert space has a unique representing vector of the same norm.

L(v)=(v,u)\quad\text{for all }v,\qquad \|L\|_{V^*}=\|u\|_V.

Assumptions & context

A complete real or complex inner-product space and a continuous linear functional.

Source

Larsson & Thomée. Partial differential equations with numerical methods.

Theorem A.1 · printed p. 228

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem riesz_representation
    {𝕜 V : Type*} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V]
    [CompleteSpace V] (L : V →L[𝕜] 𝕜) :
    (∃! u : V, ∀ v : V, L v = bookInner v u) ∧
    (∀ u : V, (∀ v : V, L v = bookInner v u) → ‖L‖ = ‖u‖) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.AppendixA

/-- The book's scalar product `(v, u)`, which is linear in its FIRST argument.
The source's identity `L(v) = (v, u)`, with `L` linear, forces linearity of `(·, u)` in the
first slot. In Mathlib's convention (conjugate-linear in the first slot) this is `inner 𝕜 u v`.
For `𝕜 = ℝ` the two conventions coincide. -/
def bookInner {𝕜 V : Type*} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V]
    (v u : V) : 𝕜 :=
  inner 𝕜 u v

/-- Theorem A.1 (Riesz' representation theorem).
Let `V` be a Hilbert space with scalar product `(·,·)`. For each bounded linear
functional `L` on `V` there is a unique `u ∈ V` with `L(v) = (v, u)` for all `v ∈ V`.
Moreover `‖L‖_{V*} = ‖u‖_V` (A.10).
Here a Hilbert space is a complete inner product space over `𝕜 ∈ {ℝ, ℂ}`, a bounded
linear functional is an element of `V →L[𝕜] 𝕜`, and `‖L‖_{V*}` is its operator norm. -/
theorem riesz_representation
    {𝕜 V : Type*} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V]
    [CompleteSpace V] (L : V →L[𝕜] 𝕜) :
    (∃! u : V, ∀ v : V, L v = bookInner v u) ∧
    (∀ u : V, (∀ v : V, L v = bookInner v u) → ‖L‖ = ‖u‖) := by
  sorry

end PDETextbook.AppendixA

How to read the formalization

The book's convention makes the inner product linear in its first argument; the Lean wrapper makes this convention explicit.

← Back to all statements