Orthonormal coordinates

This module describes coordinates adapted to a vector in a real inner product space and rotated coordinates in a complex inner product space.

For an orthonormal basis b, the i-th coordinate functional of the underlying basis is the inner product with b i.

In a finite-dimensional real inner product space, an orthonormal coordinate system can be chosen so that the inner product with a given vector is its norm times any prescribed coordinate.

For an orthonormal basis b of a complex inner product space E, indexed by a finite type ι, every v : E has the complex coordinates ⟪b j, v⟫:

• Each holomorphic quadratic form ∑ⱼ c j ⟪b j, v⟫² in these coordinates is v ↦ Q v v for a continuous complex bilinear form Q.
• For units ω j, the real and imaginary parts of the rotated coordinates conj (ω j) ⟪b j, v⟫ are real coordinates on E: they form a real linear equivalence E ≃ₗ[ℝ] (ι ⊕ ι → ℝ). Rotating each coordinate so that c j ω j² is real diagonalizes the real quadratic form Re (∑ⱼ c j ⟪b j, v⟫²) in these real coordinates.

Main definitions

• OrthonormalBasis.rotatedRealCoords: the real and imaginary parts of the rotated coordinates conj (ω j) ⟪b j, v⟫, as a real linear equivalence E ≃ₗ[ℝ] (ι ⊕ ι → ℝ).

Main statements

• OrthonormalBasis.toBasis_coord: the coordinate functional b.toBasis.coord i is innerₛₗ 𝕜 (b i).
• OrthonormalBasis.repr_apply_of_eigenbasis: in an orthonormal eigenbasis of a linear map S, the coordinates of S x are those of x scaled by the eigenvalues.
• TauCeti.exists_linearIsometryEquiv_inner_eq_norm_mul_eval: for a vector v and a prescribed coordinate i, there is a linear isometry equivalence f with ⟪v, x⟫ = ‖v‖ * f x i for all x.
• OrthonormalBasis.exists_apply_self_eq_sum_mul_inner_sq: ∑ⱼ c j ⟪b j, v⟫² is Q v v for a continuous complex bilinear form Q.

theorem TauCeti.exists_linearIsometryEquiv_inner_eq_norm_mul_eval {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (i : Fin (Module.finrank ℝ E)) : ∃ (f : E ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (Module.finrank ℝ E))), ∀ (x : E), inner ℝ v x = ‖v‖ * (f x).ofLp i

Choose orthonormal coordinates in which the inner product with v is its norm times the prescribed coordinate. This also holds for v = 0.

@[simp]

theorem OrthonormalBasis.toBasis_coord {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) : b.toBasis.coord i = (innerₛₗ 𝕜) (b i)

The i-th coordinate functional of an orthonormal basis is the inner product with its i-th vector.

theorem OrthonormalBasis.toBasis_coord_real {ι : Type u_3} [Fintype ι] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (b : OrthonormalBasis ι ℝ F) (i : ι) : b.toBasis.coord i = (innerₗ F) (b i)

The coordinate functional of a real orthonormal basis, expressed using the real bilinear inner product.

theorem OrthonormalBasis.repr_apply_of_eigenbasis {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (S : E →ₗ[𝕜] E) {μ : ι → 𝕜} (hb : ∀ (i : ι), S (b i) = μ i • b i) (x : E) (i : ι) : (b.repr (S x)).ofLp i = μ i * (b.repr x).ofLp i

The coordinates of S x in an orthonormal eigenbasis of S are the coordinates of x scaled by the eigenvalues.

theorem OrthonormalBasis.exists_apply_self_eq_sum_mul_inner_sq {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Fintype ι] (b : OrthonormalBasis ι ℂ E) (c : ι → ℂ) : ∃ (Q : E →L[ℂ] E →L[ℂ] ℂ), ∀ (v : E), (Q v) v = ∑ j : ι, c j * inner ℂ (b j) v ^ 2

The holomorphic quadratic form ∑ⱼ c j ⟪b j, z⟫² is z ↦ Q z z for a continuous complex bilinear form Q.

noncomputable def OrthonormalBasis.rotatedRealCoords {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Fintype ι] (b : OrthonormalBasis ι ℂ E) (ω : ι → ℂ) (hω : ∀ (j : ι), ω j * (starRingEnd ℂ) (ω j) = 1) : E ≃ₗ[ℝ] ι ⊕ ι → ℝ

The real and imaginary parts of the coordinates conj (ω j) ⟪b j, v⟫ in an orthonormal basis b, rotated by units ω j, as a real linear equivalence.

@[simp]

theorem OrthonormalBasis.rotatedRealCoords_apply_inl {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Fintype ι] (b : OrthonormalBasis ι ℂ E) (ω : ι → ℂ) (hω : ∀ (j : ι), ω j * (starRingEnd ℂ) (ω j) = 1) (v : E) (j : ι) : (b.rotatedRealCoords ω hω) v (Sum.inl j) = ((starRingEnd ℂ) (ω j) * inner ℂ (b j) v).re

The Sum.inl j coordinate of rotatedRealCoords is the real part of conj (ω j) ⟪b j, v⟫.

@[simp]

theorem OrthonormalBasis.rotatedRealCoords_apply_inr {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Fintype ι] (b : OrthonormalBasis ι ℂ E) (ω : ι → ℂ) (hω : ∀ (j : ι), ω j * (starRingEnd ℂ) (ω j) = 1) (v : E) (j : ι) : (b.rotatedRealCoords ω hω) v (Sum.inr j) = ((starRingEnd ℂ) (ω j) * inner ℂ (b j) v).im

The Sum.inr j coordinate of rotatedRealCoords is the imaginary part of conj (ω j) ⟪b j, v⟫.

@[simp]

theorem OrthonormalBasis.rotatedRealCoords_symm_apply {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Fintype ι] (b : OrthonormalBasis ι ℂ E) (ω : ι → ℂ) (hω : ∀ (j : ι), ω j * (starRingEnd ℂ) (ω j) = 1) (u : ι ⊕ ι → ℝ) : (b.rotatedRealCoords ω hω).symm u = ∑ j : ι, (ω j * { re := u (Sum.inl j), im := u (Sum.inr j) }) • b j

The inverse of rotatedRealCoords sends real coordinates u to the vector whose rotated coordinate conj (ω j) ⟪b j, v⟫ is u (Sum.inl j) + u (Sum.inr j) i.