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

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

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

noncomputable 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).

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

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

@[simp]

theorem ContinuousLinearMap.toLinearMap_innerSL_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : ↑((innerSL 𝕜) v) = (innerₛₗ 𝕜) v

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

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

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

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

noncomputable def InnerProductSpace.rankOne (𝕜 : Type u_4) {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] : E →L[𝕜] F →L⋆[𝕜] F →L[𝕜] E

A rank-one operator on an inner product space is given by x ↦ y ↦ z ↦ ⟪y, z⟫ • x.

This is also sometimes referred to as an outer product of vectors on a Hilbert space. This corresponds to the matrix outer product Matrix.vecMulVec, see InnerProductSpace.toMatrix_rankOne and InnerProductSpace.symm_toEuclideanLin_rankOne in Mathlib/Analysis/InnerProductSpace/PiL2.lean.

theorem InnerProductSpace.rankOne_def {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y : F) : ((rankOne 𝕜) x) y = ((innerSL 𝕜) y).smulRight x

theorem InnerProductSpace.rankOne_def' {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y : F) : ((rankOne 𝕜) x) y = (ContinuousLinearMap.toSpanSingleton 𝕜 x).comp ((innerSL 𝕜) y)

theorem InnerProductSpace.toLinearMap_rankOne {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y : F) : ↑(((rankOne 𝕜) x) y) = ((innerₛₗ 𝕜) y).smulRight x

@[simp]

theorem InnerProductSpace.norm_rankOne {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y : F) : ‖((rankOne 𝕜) x) y‖ = ‖x‖ * ‖y‖

@[simp]

theorem InnerProductSpace.nnnorm_rankOne {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y : F) : ‖((rankOne 𝕜) x) y‖₊ = ‖x‖₊ * ‖y‖₊

@[simp]

theorem InnerProductSpace.enorm_rankOne {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y : F) : ‖((rankOne 𝕜) x) y‖ₑ = ‖x‖ₑ * ‖y‖ₑ

@[simp]

theorem InnerProductSpace.rankOne_apply {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y z : F) : (((rankOne 𝕜) x) y) z = inner 𝕜 y z • x

theorem InnerProductSpace.comp_rankOne {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] {G : Type u_8} [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (x : E) (y : F) (f : E →L[𝕜] G) : f.comp (((rankOne 𝕜) x) y) = ((rankOne 𝕜) (f x)) y

theorem InnerProductSpace.isIdempotentElem_rankOne_self {𝕜 : Type u_4} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] {x : F} (hx : ‖x‖ = 1) : IsIdempotentElem (((rankOne 𝕜) x) x)

@[simp]

theorem InnerProductSpace.rankOne_one_right_eq_toSpanSingleton {𝕜 : Type u_4} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : F) : ((rankOne 𝕜) x) 1 = ContinuousLinearMap.toSpanSingleton 𝕜 x

@[simp]

theorem InnerProductSpace.rankOne_one_left_eq_innerSL {𝕜 : Type u_4} {F : Type u_6} [RCLike 𝕜] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : F) : ((rankOne 𝕜) 1) x = (innerSL 𝕜) x

theorem InnerProductSpace.rankOne_comp_rankOne {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] [SeminormedAddCommGroup G] [InnerProductSpace 𝕜 G] (x : E) (y z : F) (w : G) : (((rankOne 𝕜) x) y).comp (((rankOne 𝕜) z) w) = inner 𝕜 y z • ((rankOne 𝕜) x) w

theorem InnerProductSpace.inner_left_rankOne_apply {𝕜 : Type u_4} {F : Type u_6} {G : Type u_7} [RCLike 𝕜] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] [SeminormedAddCommGroup G] [InnerProductSpace 𝕜 G] (x : F) (y z : G) (w : F) : inner 𝕜 ((((rankOne 𝕜) x) y) z) w = inner 𝕜 z y * inner 𝕜 x w

theorem InnerProductSpace.inner_right_rankOne_apply {𝕜 : Type u_4} {F : Type u_6} {G : Type u_7} [RCLike 𝕜] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] [SeminormedAddCommGroup G] [InnerProductSpace 𝕜 G] (x y : F) (z w : G) : inner 𝕜 x ((((rankOne 𝕜) y) z) w) = inner 𝕜 x y * inner 𝕜 z w

@[simp]

theorem InnerProductSpace.rankOne_eq_zero {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_8} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {x : E} {y : F} : ((rankOne 𝕜) x) y = 0 ↔ x = 0 ∨ y = 0

theorem InnerProductSpace.rankOne_ne_zero {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_8} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {x : E} {y : F} (hx : x ≠ 0) (hy : y ≠ 0) : ((rankOne 𝕜) x) y ≠ 0

theorem InnerProductSpace.isIdempotentElem_rankOne_self_iff {𝕜 : Type u_4} [RCLike 𝕜] {F : Type u_8} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {x : F} (hx : x ≠ 0) : IsIdempotentElem (((rankOne 𝕜) x) x) ↔ ‖x‖ = 1

theorem InnerProductSpace.rankOne_eq_rankOne_iff_comm {𝕜 : Type u_4} [RCLike 𝕜] {F : Type u_8} {H : Type u_9} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {a c : F} {b d : H} : ((rankOne 𝕜) a) b = ((rankOne 𝕜) c) d ↔ ((rankOne 𝕜) b) a = ((rankOne 𝕜) d) c

theorem InnerProductSpace.exists_of_rankOne_eq_rankOne {𝕜 : Type u_4} [RCLike 𝕜] {F : Type u_8} {H : Type u_9} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {a c : F} {b d : H} (ha : a ≠ 0) (hb : b ≠ 0) (h : ((rankOne 𝕜) a) b = ((rankOne 𝕜) c) d) : ∃ (α : 𝕜) (β : 𝕜) (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d

theorem ContinuousLinearMap.opNorm_le_of_re_inner_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →L[𝕜] F} {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → RCLike.re (inner 𝕜 (T x) y) ≤ C) : ‖T‖ ≤ C