# 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

source
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.

source
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
source
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`.

source
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`.

source
@[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.

source
@[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.

source
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.

source
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' := ⋯ }

Instances For

source
@[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
source
@[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
source
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' := ⋯ }

Instances For

source
@[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
source
@[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
source
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.

source
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) ⋯ ⋯ ⋯ ⋯

Instances For

source
@[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
source
@[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
source
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ₛₗ ℝ

Instances For

source
@[simp]
theorem flip_innerₗ (F : Type u_3) [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] :
(innerₗ F).flip = innerₗ F
source
@[simp]
theorem innerₗ_apply_apply {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (v w : F) :
((innerₗ F) v) w = inner ℝ v w
source
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 ⋯

Instances For

source
@[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
source
@[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
source
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 𝕜)

Instances For

source
@[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
source
@[simp]
theorem flip_innerSL_real (F : Type u_3) [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] :
(innerSL ℝ).flip = innerSL ℝ
source
@[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`.

source
@[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`.

source
@[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`.

source
@[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`.

source
@[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`.

source
@[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`.

source
@[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`.

source
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.

Instances For

source
@[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
source
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‖
source
@[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`.

source
theorem norm_innerSL_le (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
‖innerSL 𝕜‖ ≤ 1
source
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.

source
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)

Instances For

source
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)
source
theorem ContinuousLinearMap.reApplyInnerSelf_continuous {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) :
Continuous T.reApplyInnerSelf
source
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