The Riesz isomorphism and the positive dual metric

On a Hilbert space E, the Riesz isomorphism InnerProductSpace.toDual 𝕜 E is the map innerSL 𝕜 : E →L⋆[𝕜] StrongDual 𝕜 E, upgraded to a conjugate-linear isometric equivalence. So its inverse undoes innerSL on either side. Over ℝ, the Riesz representatives of the real and imaginary parts of a complex-valued covector are its two gradients.

The Riesz operator InnerProductSpace.continuousLinearMapOfBilin B of a sesquilinear form B depends continuously on B. Over ℝ, the Riesz operator of a bilinear form k is natural: pulling k back along a linear isometry equivalence conjugates it.

In finite dimension, InnerProductSpace.dualMetric is the positive Hermitian form on the algebraic dual transported through Riesz duality. Since Riesz duality is conjugate-linear, its formula reverses the two slots. For these metrics, the adjoint of the transpose T.dualMap is the transpose of the Hermitian adjoint, T.adjoint.dualMap. No inner product instance on the algebraic dual is installed.

Main results

• InnerProductSpace.toDual_symm_innerSL: (toDual 𝕜 E).symm (innerSL 𝕜 w) = w.
• InnerProductSpace.innerSL_toDual_symm: innerSL 𝕜 ((toDual 𝕜 E).symm q) = q.
• InnerProductSpace.apply_toDual_symm_eq_conj: β(α♯) = conj (α(β♯)), writing α♯ for (toDual 𝕜 E).symm α.
• InnerProductSpace.apply_toDual_symm_self: q(q♯) = ‖q‖².
• InnerProductSpace.toDualSymmL: over ℝ, the inverse Riesz map q ↦ q♯ as a continuous linear map.
• InnerProductSpace.isInvertible_of_apply_apply_eq_mul_inner: over ℝ, a bilinear form that is a nonzero multiple of the inner product is invertible as a map to the dual.
• InnerProductSpace.continuousLinearMapOfBilin_innerSL: the Riesz operator of the real inner product is the identity.
• InnerProductSpace.continuous_continuousLinearMapOfBilin: the Riesz operator depends continuously on the sesquilinear form.
• InnerProductSpace.ker_continuousLinearMapOfBilin: the Riesz operator of a form has the kernel of the form.
• InnerProductSpace.continuousLinearMapOfBilin_neg: the Riesz operator of -B is the negative of that of B.
• InnerProductSpace.adjoint_continuousLinearMapOfBilin: over ℝ, the adjoint of the Riesz operator represents the transposed form.
• InnerProductSpace.isSelfAdjoint_continuousLinearMapOfBilin and InnerProductSpace.isUnit_continuousLinearMapOfBilin: over ℝ, the Riesz operator of a symmetric form is self-adjoint, and in finite dimension that of a nondegenerate form is invertible.
• InnerProductSpace.isSymmetric_continuousLinearMapOfBilin: over ℝ, the Riesz operator of a symmetric form is symmetric.
• ContinuousLinearMap.continuousLinearMapOfBilin_bilinearComp: pulling a real bilinear form back along a linear isometry equivalence conjugates its Riesz operator.
• ContinuousLinearMap.reGradient P, ContinuousLinearMap.imGradient P: the vectors representing the real and imaginary parts of a complex-valued covector P, with ⟪P.reGradient, v⟫ = Re (P v), ⟪P.imGradient, v⟫ = Im (P v) and norms at most ‖P‖.
• InnerProductSpace.dualMetric: the Hermitian form on the algebraic dual transported by Riesz.
• InnerProductSpace.dualMetric_innerₛₗ: its value on Riesz functionals is ⟪y, x⟫.
• InnerProductSpace.isPosSemidef_dualMetric: the dual metric is Hermitian and positive semidefinite.
• InnerProductSpace.dualMetric_self_eq_zero_iff: a functional has zero square norm iff it is zero.
• LinearMap.dualMetric_dualMap_left: transposition and Hermitian adjunction commute.

@[simp]

theorem InnerProductSpace.continuousLinearMapOfBilin_innerSL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : continuousLinearMapOfBilin (innerSL ℝ) = 1

The Riesz operator of the reference inner product is the identity.

theorem InnerProductSpace.contDiff_continuousLinearMapOfBilin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {n : WithTop ℕ∞} : ContDiff ℝ n continuousLinearMapOfBilin

The Riesz operator depends smoothly on a bounded real bilinear form on a Hilbert space. No finite-dimensionality or positivity is required.

@[simp]

theorem InnerProductSpace.toDual_symm_innerSL {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (w : E) : (toDual 𝕜 E).symm ((innerSL 𝕜) w) = w

The inverse Riesz isomorphism sends the functional innerSL 𝕜 w = ⟪w, ·⟫ back to w.

@[simp]

theorem InnerProductSpace.innerSL_toDual_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (q : StrongDual 𝕜 E) : (innerSL 𝕜) ((toDual 𝕜 E).symm q) = q

The functional ⟪(toDual 𝕜 E).symm q, ·⟫ represented by the inverse Riesz isomorphism is q.

theorem InnerProductSpace.continuous_continuousLinearMapOfBilin {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : Continuous continuousLinearMapOfBilin

The Riesz operator continuousLinearMapOfBilin B depends continuously on the sesquilinear form B: it is the composite of B with the inverse Riesz isomorphism.

@[simp]

theorem InnerProductSpace.ker_continuousLinearMapOfBilin {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) : (↑(continuousLinearMapOfBilin B)).ker = (↑B).ker

The Fréchet–Riesz operator of a bounded sesquilinear form has the same kernel as the form: u lies in it exactly when B(u, v) = 0 for every v.

@[simp]

theorem InnerProductSpace.continuousLinearMapOfBilin_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) : continuousLinearMapOfBilin (-B) = -continuousLinearMapOfBilin B

The Fréchet–Riesz operator of the negative of a form is the negative of its Riesz operator.

theorem InnerProductSpace.apply_toDual_symm_eq_conj {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (α β : StrongDual 𝕜 E) : β ((toDual 𝕜 E).symm α) = (starRingEnd 𝕜) (α ((toDual 𝕜 E).symm β))

Evaluating functionals at each other's Riesz representatives is conjugate-symmetric: β(α♯) = conj (α(β♯)). Over ℝ this says β(α♯) = α(β♯).

theorem InnerProductSpace.apply_toDual_symm_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (q : StrongDual 𝕜 E) : q ((toDual 𝕜 E).symm q) = ↑‖q‖ ^ 2

A functional evaluated at its own Riesz representative is its squared norm.

noncomputable def InnerProductSpace.toDualSymmL {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] : StrongDual ℝ F →L[ℝ] F

On a real Hilbert space the inverse Riesz isomorphism q ↦ q♯ = (toDual ℝ F).symm q is linear; this is it as a continuous linear map.

@[simp]

theorem InnerProductSpace.toDualSymmL_apply {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (q : StrongDual ℝ F) : toDualSymmL q = (toDual ℝ F).symm q

theorem InnerProductSpace.isInvertible_of_apply_apply_eq_mul_inner {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {c : ℝ} (hc : c ≠ 0) {B : F →L[ℝ] StrongDual ℝ F} (hB : ∀ (b a : F), (B b) a = c * inner ℝ b a) : B.IsInvertible

On a real Hilbert space, a bounded bilinear form B(b, a) = c ⟪b, a⟫ with c ≠ 0, viewed as a map to the dual, is invertible: it is c times the Riesz isomorphism.

@[simp]

theorem InnerProductSpace.adjoint_continuousLinearMapOfBilin {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (B : F →L[ℝ] F →L[ℝ] ℝ) : ContinuousLinearMap.adjoint (continuousLinearMapOfBilin B) = continuousLinearMapOfBilin B.flip

The adjoint of the Fréchet–Riesz operator of a real bilinear form represents the transposed form.

theorem InnerProductSpace.isSelfAdjoint_continuousLinearMapOfBilin {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {B : F →L[ℝ] F →L[ℝ] ℝ} (hB : ∀ (v w : F), (B v) w = (B w) v) : IsSelfAdjoint (continuousLinearMapOfBilin B)

The Fréchet–Riesz operator of a symmetric real bilinear form is self-adjoint.

theorem InnerProductSpace.isUnit_continuousLinearMapOfBilin {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] [FiniteDimensional ℝ F] {B : F →L[ℝ] F →L[ℝ] ℝ} (hB : Function.Injective ⇑B) : IsUnit (continuousLinearMapOfBilin B)

In finite dimension, the Fréchet–Riesz operator of a nondegenerate real bilinear form is invertible.

theorem InnerProductSpace.isSymmetric_continuousLinearMapOfBilin {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {B : F →L[ℝ] F →L[ℝ] ℝ} (hB : ∀ (u v : F), (B u) v = (B v) u) : (↑(continuousLinearMapOfBilin B)).IsSymmetric

The Fréchet–Riesz operator of a symmetric real bilinear form is symmetric.

theorem InnerProductSpace.instCompleteSpace_tauCeti (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : CompleteSpace E

noncomputable def InnerProductSpace.dualMetric (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : Module.Dual 𝕜 E →ₗ⋆[𝕜] Module.Dual 𝕜 E →ₗ[𝕜] 𝕜

The Hermitian metric on the algebraic dual transported through the conjugate-linear Riesz isomorphism. Its value on ⟪x, ·⟫ and ⟪y, ·⟫ is ⟪y, x⟫.

theorem InnerProductSpace.dualMetric_apply (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (φ ψ : Module.Dual 𝕜 E) : ((dualMetric 𝕜 E) φ) ψ = inner 𝕜 ((toDual 𝕜 E).symm (LinearMap.toContinuousLinearMap ψ)) ((toDual 𝕜 E).symm (LinearMap.toContinuousLinearMap φ))

Evaluation of the dual metric in terms of the inverse Riesz isomorphism.

@[simp]

theorem InnerProductSpace.dualMetric_innerₛₗ (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (x y : E) : ((dualMetric 𝕜 E) ((innerₛₗ 𝕜) x)) ((innerₛₗ 𝕜) y) = inner 𝕜 y x

Riesz duality is antiunitary for the dual metric.

theorem Module.Dual.existsUnique_innerₛₗ_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (φ : Dual 𝕜 E) : ∃! x : E, (innerₛₗ 𝕜) x = φ

Every algebraic functional on a finite-dimensional inner product space is represented by a unique vector. This is the algebraic form of Riesz representation.

theorem InnerProductSpace.isPosSemidef_dualMetric (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : (dualMetric 𝕜 E).IsPosSemidef

The transported dual metric is Hermitian and positive semidefinite.

@[simp]

theorem InnerProductSpace.dualMetric_self_eq_zero_iff (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (φ : Module.Dual 𝕜 E) : ((dualMetric 𝕜 E) φ) φ = 0 ↔ φ = 0

The dual metric is definite, including on the zero space.

theorem InnerProductSpace.instCompleteSpace_tauCeti_1 {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] : CompleteSpace F

@[simp]

theorem LinearMap.dualMap_innerₛₗ {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) (x : F) : T.dualMap ((innerₛₗ 𝕜) x) = (innerₛₗ 𝕜) ((adjoint T) x)

The transpose of an operator acts on Riesz functionals through its Hermitian adjoint.

theorem LinearMap.dualMetric_dualMap_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) (φ : Module.Dual 𝕜 F) (ψ : Module.Dual 𝕜 E) : ((InnerProductSpace.dualMetric 𝕜 E) (T.dualMap φ)) ψ = ((InnerProductSpace.dualMetric 𝕜 F) φ) ((adjoint T).dualMap ψ)

Transposition and Hermitian adjunction commute for the transported dual metrics.

theorem ContinuousLinearMap.continuousLinearMapOfBilin_bilinearComp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (e : E ≃ₗᵢ[ℝ] F) (k : F →L[ℝ] F →L[ℝ] ℝ) : InnerProductSpace.continuousLinearMapOfBilin (k.bilinearComp ↑↑e ↑↑e) = e.symm.conjStarAlgEquiv (InnerProductSpace.continuousLinearMapOfBilin k)

Pulling a bilinear form k on F back along a linear isometry equivalence e : E ≃ₗᵢ[ℝ] F conjugates its Riesz operator by e.

noncomputable def ContinuousLinearMap.reGradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : E →L[ℝ] ℂ) : E

The vector representing the real part of a complex-valued covector P: ⟪P.reGradient, v⟫ = Re (P v).

noncomputable def ContinuousLinearMap.imGradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : E →L[ℝ] ℂ) : E

The vector representing the imaginary part of a complex-valued covector P: ⟪P.imGradient, v⟫ = Im (P v).

@[simp]

theorem ContinuousLinearMap.inner_reGradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : E →L[ℝ] ℂ) (v : E) : inner ℝ P.reGradient v = (P v).re

⟪p₁, v⟫ = Re (P v) for the gradient p₁ of the real part of P.

@[simp]

theorem ContinuousLinearMap.inner_imGradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : E →L[ℝ] ℂ) (v : E) : inner ℝ P.imGradient v = (P v).im

⟪p₂, v⟫ = Im (P v) for the gradient p₂ of the imaginary part of P.

theorem ContinuousLinearMap.norm_reGradient_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : E →L[ℝ] ℂ) : ‖P.reGradient‖ ≤ ‖P‖

The gradient of the real part of P has norm at most ‖P‖.

theorem ContinuousLinearMap.norm_imGradient_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : E →L[ℝ] ℂ) : ‖P.imGradient‖ ≤ ‖P‖

The gradient of the imaginary part of P has norm at most ‖P‖.