class HilbertSpace.IsHilbertSpace (V : Type u_1) [NormedAddCommGroup V] extends InnerProductSpace ℂ V, CompleteSpace V : Type u_1

A Hilbert space is a complex inner product space that is complete with respect to the norm induced by the inner product. This is Definition 5.1 of Melrose, packaged as a type class combining InnerProductSpace ℂ V with CompleteSpace V.

• smul : ℂ → V → V
• mul_smul (x y : ℂ) (b : V) : (x * y) • b = x • y • b
• one_smul (b : V) : 1 • b = b
• smul_zero (a : ℂ) : a • 0 = 0
• smul_add (a : ℂ) (x y : V) : a • (x + y) = a • x + a • y
• add_smul (r s : ℂ) (x : V) : (r + s) • x = r • x + s • x
• zero_smul (x : V) : 0 • x = 0
• norm_smul_le (a : ℂ) (b : V) : ‖a • b‖ ≤ ‖a‖ * ‖b‖
• inner : V → V → ℂ
• norm_sq_eq_re_inner (x : V) : ‖x‖ ^ 2 = RCLike.re (inner ℂ x x)
• conj_inner_symm (x y : V) : (starRingEnd ℂ) (inner ℂ y x) = inner ℂ x y
• add_left (x y z : V) : inner ℂ (x + y) z = inner ℂ x z + inner ℂ y z
• smul_left (x y : V) (r : ℂ) : inner ℂ (r • x) y = (starRingEnd ℂ) r * inner ℂ x y
• complete {f : Filter V} : Cauchy f → ∃ (x : V), f ≤ nhds x

theorem HilbertSpace.exists_smallest_norm_of_closed_convex {V : Type u_1} [NormedAddCommGroup V] [IsHilbertSpace V] {C : Set V} (hne : C.Nonempty) (hclosed : IsClosed C) (hconvex : Convex ℝ C) : ∃ v ∈ C, ‖v‖ = ⨅ (w : ↑C), ‖↑w‖

Existence part of the closest point theorem (Lemma 5.2 of Melrose): every nonempty closed convex subset of a Hilbert space contains an element of minimal norm, attaining the infimum ⨅ w : C, ‖w‖.

theorem HilbertSpace.unique_smallest_norm_of_closed_convex {V : Type u_1} [NormedAddCommGroup V] [IsHilbertSpace V] {C : Set V} (hne : C.Nonempty) (hclosed : IsClosed C) (hconvex : Convex ℝ C) {v v' : V} (hv : v ∈ C) (hv' : v' ∈ C) (hmin_v : ‖v‖ = ⨅ (w : ↑C), ‖↑w‖) (hmin_v' : ‖v'‖ = ⨅ (w : ↑C), ‖↑w‖) : v = v'

Uniqueness part of the closest point theorem (Lemma 5.2 of Melrose): two elements of a closed convex subset of a Hilbert space that both attain the minimum norm must coincide. The proof uses the parallelogram law applied to their midpoint, which also lies in the set.

theorem HilbertSpace.exists_unique_smallest_norm_of_closed_convex {V : Type u_1} [NormedAddCommGroup V] [IsHilbertSpace V] {C : Set V} (hne : C.Nonempty) (hclosed : IsClosed C) (hconvex : Convex ℝ C) : ∃! v : V, v ∈ C ∧ ‖v‖ = ⨅ (w : ↑C), ‖↑w‖

Existence and uniqueness of the minimum-norm point in a nonempty closed convex subset of a Hilbert space (Lemma 5.2 of Melrose), packaged as an ∃! statement combining exists_smallest_norm_of_closed_convex and unique_smallest_norm_of_closed_convex.

theorem HilbertSpace.riesz_representation {V : Type u_1} [NormedAddCommGroup V] [IsHilbertSpace V] (L : V →L[ℂ] ℂ) : ∃! v : V, ∀ (u : V), L u = inner ℂ v u

Riesz representation theorem (Proposition 5.3 of Melrose): every continuous linear functional L : V →L[ℂ] ℂ on a Hilbert space is represented by a unique vector v via L u = ⟪v, u⟫.

theorem HilbertSpace.l2_dual_eq_integral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (L : ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ℂ) : ∃ (g : ↥(MeasureTheory.Lp ℂ 2 μ)), ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)), L f = ∫ (a : α), ↑↑f a * (starRingEnd ℂ) (↑↑g a) ∂μ

Concrete Riesz representation for the dual of L²(μ; ℂ): every continuous linear functional on L² is given by integration against (the conjugate of) some L² function g. This is the specialisation of Proposition 5.3 to the Hilbert space L²(α, μ; ℂ).