Linear maps on inner product spaces

This file studies linear maps on inner product spaces.

Main results

• We define innerSL as the inner product bundled as a continuous sesquilinear map, and innerₛₗ for the non-continuous version.
• We prove a general polarization identity for linear maps (inner_map_polarization)
• We show that a linear map preserving the inner product is an isometry (LinearMap.isometryOfInner) and conversely an isometry preserves the inner product (LinearIsometry.inner_map_map).

Tags

inner product space, Hilbert space, norm

theorem inner_map_polarization {V : Type u_4} [SeminormedAddCommGroup V] [InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) (x y : V) : inner ℂ (T y) x = (inner ℂ (T (x + y)) (x + y) - inner ℂ (T (x - y)) (x - y) + Complex.I * inner ℂ (T (x + Complex.I • y)) (x + Complex.I • y) - Complex.I * inner ℂ (T (x - Complex.I • y)) (x - Complex.I • y)) / 4

A complex polarization identity, with a linear map.

theorem inner_map_polarization' {V : Type u_4} [SeminormedAddCommGroup V] [InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) (x y : V) : inner ℂ (T x) y = (inner ℂ (T (x + y)) (x + y) - inner ℂ (T (x - y)) (x - y) - Complex.I * inner ℂ (T (x + Complex.I • y)) (x + Complex.I • y) + Complex.I * inner ℂ (T (x - Complex.I • y)) (x - Complex.I • y)) / 4

theorem inner_map_self_eq_zero {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) : (∀ (x : V), inner ℂ (T x) x = 0) ↔ T = 0

A linear map T is zero, if and only if the identity ⟪T x, x⟫_ℂ = 0 holds for all x.

theorem ext_inner_map {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (S T : V →ₗ[ℂ] V) : (∀ (x : V), inner ℂ (S x) x = inner ℂ (T x) x) ↔ S = T

Two linear maps S and T are equal, if and only if the identity ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ holds for all x.

@[simp]

theorem LinearIsometry.inner_map_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (x y : E) : inner 𝕜 (f x) (f y) = inner 𝕜 x y

A linear isometry preserves the inner product.

@[simp]

theorem LinearIsometryEquiv.inner_map_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (x y : E) : inner 𝕜 (f x) (f y) = inner 𝕜 x y

A linear isometric equivalence preserves the inner product.

theorem LinearIsometryEquiv.inner_map_eq_flip {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (x : E) (y : E') : inner 𝕜 (f x) y = inner 𝕜 x (f.symm y)

The adjoint of a linear isometric equivalence is its inverse.

def LinearMap.isometryOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y) : E →ₗᵢ[𝕜] E'

A linear map that preserves the inner product is a linear isometry.

Equations

• f.isometryOfInner h = { toLinearMap := f, norm_map' := ⋯ }

@[simp]

theorem LinearMap.coe_isometryOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y) : ⇑(f.isometryOfInner h) = ⇑f

@[simp]

theorem LinearMap.isometryOfInner_toLinearMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y) : (f.isometryOfInner h).toLinearMap = f

def LinearEquiv.isometryOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y) : E ≃ₗᵢ[𝕜] E'

A linear equivalence that preserves the inner product is a linear isometric equivalence.

Equations

• f.isometryOfInner h = { toLinearEquiv := f, norm_map' := ⋯ }

@[simp]

theorem LinearEquiv.coe_isometryOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y) : ⇑(f.isometryOfInner h) = ⇑f

@[simp]

theorem LinearEquiv.isometryOfInner_toLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') (h : ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y) : (f.isometryOfInner h).toLinearEquiv = f

theorem LinearMap.norm_map_iff_inner_map_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {F : Type u_9} [FunLike F E E'] [LinearMapClass F 𝕜 E E'] (f : F) : (∀ (x : E), ‖f x‖ = ‖x‖) ↔ ∀ (x y : E), inner 𝕜 (f x) (f y) = inner 𝕜 x y

A linear map is an isometry if and it preserves the inner product.

def innerₛₗ (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜

The inner product as a sesquilinear map.

Equations

• innerₛₗ 𝕜 = LinearMap.mk₂'ₛₗ (starRingEnd 𝕜) (RingHom.id 𝕜) (fun (v w : E) => inner 𝕜 v w) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem coe_innerₛₗ_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : ⇑((innerₛₗ 𝕜) v) = fun (w : E) => inner 𝕜 v w

@[simp]

theorem innerₛₗ_apply_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v w : E) : ((innerₛₗ 𝕜) v) w = inner 𝕜 v w

def innerₗ (F : Type u_3) [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] : F →ₗ[ℝ] F →ₗ[ℝ] ℝ

The inner product as a bilinear map in the real case.

Equations

• innerₗ F = innerₛₗ ℝ

@[simp]

theorem flip_innerₗ (F : Type u_3) [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] : (innerₗ F).flip = innerₗ F

@[simp]

theorem innerₗ_apply_apply {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (v w : F) : ((innerₗ F) v) w = inner ℝ v w

def innerSL (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →L⋆[𝕜] E →L[𝕜] 𝕜

The inner product as a continuous sesquilinear map. Note that toDualMap (resp. toDual) in InnerProductSpace.Dual is a version of this given as a linear isometry (resp. linear isometric equivalence).

Equations

• innerSL 𝕜 = (innerₛₗ 𝕜).mkContinuous₂ 1 ⋯

@[simp]

theorem coe_innerSL_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : ⇑((innerSL 𝕜) v) = fun (w : E) => inner 𝕜 v w

@[simp]

theorem innerSL_apply_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v w : E) : ((innerSL 𝕜) v) w = inner 𝕜 v w

def innerSLFlip (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →L[𝕜] E →L⋆[𝕜] 𝕜

The inner product as a continuous sesquilinear map, with the two arguments flipped.

Equations

• innerSLFlip 𝕜 = (ContinuousLinearMap.flipₗᵢ' E E 𝕜 (RingHom.id 𝕜) (starRingEnd 𝕜)) (innerSL 𝕜)

@[simp]

theorem innerSLFlip_apply_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) : ((innerSLFlip 𝕜) x) y = inner 𝕜 y x

@[simp]

theorem flip_innerSL_real (F : Type u_3) [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] : (innerSL ℝ).flip = innerSL ℝ

@[deprecated coe_innerₛₗ_apply (since := "2025-11-15")]

theorem innerₛₗ_apply_coe (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : ⇑((innerₛₗ 𝕜) v) = fun (w : E) => inner 𝕜 v w

Alias of coe_innerₛₗ_apply.

@[deprecated innerₛₗ_apply_apply (since := "2025-11-15")]

theorem innerₛₗ_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v w : E) : ((innerₛₗ 𝕜) v) w = inner 𝕜 v w

Alias of innerₛₗ_apply_apply.

@[deprecated innerₗ_apply_apply (since := "2025-11-15")]

theorem innerₗ_apply {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (v w : F) : ((innerₗ F) v) w = inner ℝ v w

Alias of innerₗ_apply_apply.

@[deprecated coe_innerSL_apply (since := "2025-11-15")]

theorem innerSL_apply_coe (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : ⇑((innerSL 𝕜) v) = fun (w : E) => inner 𝕜 v w

Alias of coe_innerSL_apply.

@[deprecated innerSL_apply_apply (since := "2025-11-15")]

theorem innerSL_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v w : E) : ((innerSL 𝕜) v) w = inner 𝕜 v w

Alias of innerSL_apply_apply.

@[deprecated innerSLFlip_apply_apply (since := "2025-11-15")]

theorem innerSLFlip_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) : ((innerSLFlip 𝕜) x) y = inner 𝕜 y x

Alias of innerSLFlip_apply_apply.

@[deprecated flip_innerSL_real (since := "2025-11-15")]

theorem innerSL_real_flip (F : Type u_3) [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] : (innerSL ℝ).flip = innerSL ℝ

Alias of flip_innerSL_real.

noncomputable def ContinuousLinearMap.toSesqForm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_4} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] : (E →L[𝕜] E') →L[𝕜] E' →L⋆[𝕜] E →L[𝕜] 𝕜

Given f : E →L[𝕜] E', construct the continuous sesquilinear form fun x y ↦ ⟪x, A y⟫, given as a continuous linear map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearMap.toSesqForm_apply_coe {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_4} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →L[𝕜] E') (x : E') : (toSesqForm f) x = ((innerSL 𝕜) x).comp f

theorem ContinuousLinearMap.toSesqForm_apply_norm_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E' : Type u_4} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {f : E →L[𝕜] E'} {v : E'} : ‖(toSesqForm f) v‖ ≤ ‖f‖ * ‖v‖

@[simp]

theorem innerSL_apply_norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ‖(innerSL 𝕜) x‖ = ‖x‖

innerSL is an isometry. Note that the associated LinearIsometry is defined in InnerProductSpace.Dual as toDualMap.

theorem norm_innerSL_le (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : ‖innerSL 𝕜‖ ≤ 1

theorem inner_map_complex {G : Type u_4} [SeminormedAddCommGroup G] [InnerProductSpace ℝ G] (f : G ≃ₗᵢ[ℝ] ℂ) (x y : G) : inner ℝ x y = (f y * (starRingEnd ℂ) (f x)).re

The inner product on an inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.

def ContinuousLinearMap.reApplyInnerSelf {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (x : E) : ℝ

Extract a real bilinear form from an operator T, by taking the pairing fun x ↦ re ⟪T x, x⟫.

Equations

• T.reApplyInnerSelf x = RCLike.re (inner 𝕜 (T x) x)

theorem ContinuousLinearMap.reApplyInnerSelf_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (x : E) : T.reApplyInnerSelf x = RCLike.re (inner 𝕜 (T x) x)

theorem ContinuousLinearMap.reApplyInnerSelf_continuous {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) : Continuous T.reApplyInnerSelf

theorem ContinuousLinearMap.reApplyInnerSelf_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) (x : E) {c : 𝕜} : T.reApplyInnerSelf (c • x) = ‖c‖ ^ 2 * T.reApplyInnerSelf x