Some obvious basic properties on inner product space

This files provides some useful and obvious results for linear maps and continuous linear maps.

theorem ext_inner_left_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : x = y ↔ ∀ (v : E), inner x v = inner y v

theorem inner_self_re {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ↑(RCLike.re (inner x x)) = inner x x

theorem forall_inner_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : (∀ (y : E), inner x y = 0) ↔ x = 0

theorem LinearMap.ext_iff_inner_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (p : E →ₗ[ℂ] E) (q : E →ₗ[ℂ] E) : p = q ↔ ∀ (x : E), inner (p x) x = inner (q x) x

linear maps $p,q$ are equal if and only if $\langle p x, x \rangle = \langle q x, x \rangle$ for any $x$.

theorem ContinuousLinearMap.ext_iff_inner_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (p : E →L[ℂ] E) (q : E →L[ℂ] E) : p = q ↔ ∀ (x : E), inner (p x) x = inner (q x) x

copy of linear_map.ext_iff_inner_map but for continuous linear maps

theorem ContinuousLinearMap.IsSelfAdjoint.ext_iff_inner_map {E : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} {q : E →L[𝕜] E} (hp : IsSelfAdjoint p) (hq : IsSelfAdjoint q) : p = q ↔ ∀ (x : E), inner (p x) x = inner (q x) x

Self-adjoint linear operators $p,q$ are equal if and only if $\langle p x, x \rangle_\mathbb{k} = \langle q x, x \rangle_\mathbb{k}$.

theorem isSelfAdjoint_iff_complex_inner_re_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {a : E →L[ℂ] E} : IsSelfAdjoint a ↔ ∀ (x : E), ↑(RCLike.re (inner (a x) x)) = inner (a x) x

in a complex inner product space, we have that an operator $a$ is self-adjoint if and only if $\langle a x, x \rangle_\mathbb{C}$ is real for all $x \in E$

theorem IsSelfAdjoint.adjoint {E : Type u_1} [NormedAddCommGroup E] {𝕜 : Type u_2} [RCLike 𝕜] [InnerProductSpace 𝕜 E] [CompleteSpace E] {a : E →L[𝕜] E} (ha : IsSelfAdjoint a) : IsSelfAdjoint (ContinuousLinearMap.adjoint a)

the adjoint of a self-adjoint operator is self-adjoint

theorem IsSelfAdjoint.inner_re_eq {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {a : E →L[𝕜] E} (ha : IsSelfAdjoint a) (x : E) : ↑(RCLike.re (inner (a x) x)) = inner (a x) x

for a self-adjoint operator $a$, we have $\langle a x, x \rangle_\mathbb{k}$ is real

theorem ContinuousLinearMap.inner_map_self_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p : E →L[ℂ] E} : (∀ (x : E), inner (p x) x = 0) ↔ p = 0

copy of inner_map_self_eq_zero for bounded linear maps

theorem ContinuousLinearMap.adjoint_smul {K : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [RCLike K] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace K E₁] [InnerProductSpace K E₂] [CompleteSpace E₁] [CompleteSpace E₂] (φ : E₁ →L[K] E₂) (a : K) : ContinuousLinearMap.adjoint (a • φ) = (starRingEnd K) a • ContinuousLinearMap.adjoint φ

theorem LinearMap.adjoint_smul {K : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} [RCLike K] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace K E₁] [InnerProductSpace K E₂] [FiniteDimensional K E₁] [FiniteDimensional K E₂] (φ : E₁ →ₗ[K] E₂) (a : K) : LinearMap.adjoint (a • φ) = (starRingEnd K) a • LinearMap.adjoint φ

theorem LinearMap.adjoint_one {K : Type u_2} {E : Type u_3} [RCLike K] [NormedAddCommGroup E] [InnerProductSpace K E] [FiniteDimensional K E] : LinearMap.adjoint 1 = 1

theorem inner_self_nonneg' {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} : 0 ≤ inner x x

theorem inner_self_nonpos' {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} : inner x x ≤ 0 ↔ x = 0

theorem isometry_iff_norm {E : Type u_4} {F : Type u_5} [SeminormedAddGroup E] [SeminormedAddGroup F] {e : Type u_3} [FunLike e E F] [AddMonoidHomClass e E F] (f : e) : Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖

theorem isometry_iff_norm' {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] {e : Type u_3} [FunLike e E F] [AddMonoidHomClass e E F] (f : e) : Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖

theorem isometry_iff_inner {R : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike R] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace R E] [InnerProductSpace R F] {M : Type u_3} [FunLike M E F] [LinearMapClass M R E F] (f : M) : Isometry ⇑f ↔ ∀ (x y : E), inner (f x) (f y) = inner x y

theorem isometry_iff_inner_norm' {R : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike R] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace R E] [InnerProductSpace R F] {M : Type u_3} [FunLike M E F] [LinearMapClass M R E F] (f : M) : (∀ (x : E), ‖f x‖ = ‖x‖) ↔ ∀ (x y : E), inner (f x) (f y) = inner x y

theorem seminormedAddGroup_norm_eq_norm_NormedAddCommGroup {E : Type u_3} [NormedAddCommGroup E] (x : E) : ‖x‖ = ‖x‖