English
Every continuous linear functional on a Hilbert space E arises from taking inner products with a unique vector in E; i.e., the dual is represented by E.
Русский
Каждый непрерывный линейный функционал на гильбертовом пространстве E представим как скалярное произведение с некоторым уникальным вектором из E; двойственное пространство представимо через E.
LaTeX
$$∀\ell ∈ StrongDual 𝕜 E, ∃ y ∈ E, ∀ x ∈ E, \ell(x) = ⟪y, x⟫$$
Lean4
/-- **Fréchet-Riesz representation**: any `ℓ` in the dual of a Hilbert space `E` is of the form
`fun u => ⟪y, u⟫` for some `y : E`, i.e. `toDualMap` is surjective.
-/
def toDual : E ≃ₗᵢ⋆[𝕜] StrongDual 𝕜 E :=
LinearIsometryEquiv.ofSurjective (toDualMap 𝕜 E)
(by
intro ℓ
set Y := LinearMap.ker ℓ
by_cases htriv : Y = ⊤
· have hℓ : ℓ = 0 := by
have h' := LinearMap.ker_eq_top.mp htriv
rw [← coe_zero] at h'
apply coe_injective
exact h'
exact ⟨0, by simp [hℓ]⟩
· rw [← Submodule.orthogonal_eq_bot_iff] at htriv
change Yᗮ ≠ ⊥ at htriv
rw [Submodule.ne_bot_iff] at htriv
obtain ⟨z : E, hz : z ∈ Yᗮ, z_ne_0 : z ≠ 0⟩ := htriv
refine ⟨(starRingEnd (R := 𝕜) (ℓ z) / ⟪z, z⟫) • z, ?_⟩
apply ContinuousLinearMap.ext
intro x
have h₁ : ℓ z • x - ℓ x • z ∈ Y :=
by
rw [LinearMap.mem_ker, map_sub, ContinuousLinearMap.map_smul, ContinuousLinearMap.map_smul,
Algebra.id.smul_eq_mul, Algebra.id.smul_eq_mul, mul_comm]
exact sub_self (ℓ x * ℓ z)
have h₂ : ℓ z * ⟪z, x⟫ = ℓ x * ⟪z, z⟫ :=
haveI h₃ :=
calc
0 = ⟪z, ℓ z • x - ℓ x • z⟫ := by
rw [(Y.mem_orthogonal' z).mp hz]
exact h₁
_ = ⟪z, ℓ z • x⟫ - ⟪z, ℓ x • z⟫ := by rw [inner_sub_right]
_ = ℓ z * ⟪z, x⟫ - ℓ x * ⟪z, z⟫ := by simp [inner_smul_right]
sub_eq_zero.mp h₃.symm
calc
⟪(ℓ z† / ⟪z, z⟫) • z, x⟫ = ℓ z / ⟪z, z⟫ * ⟪z, x⟫ := by simp [inner_smul_left]
_ = ℓ z * ⟪z, x⟫ / ⟪z, z⟫ := by rw [← div_mul_eq_mul_div]
_ = ℓ x * ⟪z, z⟫ / ⟪z, z⟫ := by rw [h₂]
_ = ℓ x := by field_simp [inner_self_ne_zero.2])
