Expansions and contractions against orthonormal bases

Finite sums over orthonormal bases recover linear maps from their matrix coefficients and contract tensors in orthonormal frames, for instance when tracing the Ricci tensor to scalar curvature:

• OrthonormalBasis.sum_apply_mul_inner: a linear functional ℓ satisfies ∑ i, ℓ (b i) * ⟪b i, a⟫ = ℓ a, the expansion of a in b pushed through ℓ.
• OrthonormalBasis.sum_inner_smul_rankOne: an operator is the sum of its matrix coefficients times the corresponding rank-one operators.
• OrthonormalBasis.sum_sum_inner_mul_inner_mul_inner: the two-basis expansion ⟪x, T y⟫ = ∑ᵢ ∑ⱼ ⟪x, uᵢ⟫ ⟪uᵢ, T vⱼ⟫ ⟪vⱼ, y⟫.
• OrthonormalBasis.sum_inner_self: ∑ i, ⟪b i, b i⟫ = card ι, the trace of the identity.
• OrthonormalBasis.inner_eq_sum_repr: the inner product in coordinates, ⟪x, y⟫ = ∑ i, conj (b.repr x i) * b.repr y i.
• OrthonormalBasis.real_inner_fin_two: in a real plane with orthonormal basis b, ⟪x, y⟫ = ⟪x, b₀⟫ ⟪y, b₀⟫ + ⟪x, b₁⟫ ⟪y, b₁⟫.
• Complex.isometryOfOrthonormal_symm_apply_eq_mk: in the same plane, the complex coordinate of x given by Complex.isometryOfOrthonormal b is ⟪x, b₀⟫ + i ⟪x, b₁⟫.

theorem OrthonormalBasis.sum_apply_mul_inner {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {F : Type u_4} [FunLike F E 𝕜] [LinearMapClass F 𝕜 E 𝕜] (b : OrthonormalBasis ι 𝕜 E) (ℓ : F) (a : E) : ∑ i : ι, ℓ (b i) * inner 𝕜 (b i) a = ℓ a

A linear functional is recovered from its values on an orthonormal basis: ∑ i, ℓ (b i) * ⟪b i, a⟫ = ℓ a.

theorem OrthonormalBasis.sum_inner_self {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : ∑ i : ι, inner 𝕜 (b i) (b i) = ↑(Fintype.card ι)

The vectors of an orthonormal basis have unit length, so ∑ i, ⟪b i, b i⟫ = card ι.

theorem OrthonormalBasis.inner_eq_sum_repr {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x y : E) : inner 𝕜 x y = ∑ i : ι, (starRingEnd ((fun (x : ι) => 𝕜) i)) ((b.repr x).ofLp i) * (b.repr y).ofLp i

The inner product in the coordinates of an orthonormal basis: ⟪x, y⟫ = ∑ i, conj (b.repr x i) * b.repr y i.

theorem OrthonormalBasis.real_inner_fin_two {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (b : OrthonormalBasis (Fin 2) ℝ V) (x y : V) : inner ℝ x y = inner ℝ x (b 0) * inner ℝ y (b 0) + inner ℝ x (b 1) * inner ℝ y (b 1)

The real inner product in the two coordinates of an orthonormal basis b of a plane: ⟪x, y⟫ = ⟪x, b₀⟫ ⟪y, b₀⟫ + ⟪x, b₁⟫ ⟪y, b₁⟫.

theorem OrthonormalBasis.sum_inner_smul_rankOne {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {F : Type u_4} {κ : Type u_5} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Fintype κ] (u : OrthonormalBasis ι 𝕜 E) (v : OrthonormalBasis κ 𝕜 F) (C : F →L[𝕜] E) : ∑ i : ι, ∑ j : κ, inner 𝕜 (u i) (C (v j)) • ((InnerProductSpace.rankOne 𝕜) (u i)) (v j) = C

Expansion in rank-one operators. For orthonormal bases (uᵢ) of E and (vⱼ) of F, every C : F →L[𝕜] E is the sum of its matrix coefficients ⟪uᵢ, C vⱼ⟫ times the rank-one operators rankOne 𝕜 uᵢ vⱼ : x ↦ ⟪vⱼ, x⟫ uᵢ.

theorem OrthonormalBasis.sum_sum_inner_mul_inner_mul_inner {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {F : Type u_4} {κ : Type u_5} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Fintype κ] (u : OrthonormalBasis ι 𝕜 E) (v : OrthonormalBasis κ 𝕜 F) (T : F →ₗ[𝕜] E) (x : E) (y : F) : ∑ i : ι, ∑ j : κ, inner 𝕜 x (u i) * inner 𝕜 (u i) (T (v j)) * inner 𝕜 (v j) y = inner 𝕜 x (T y)

Matrix coefficients of an inner product. For orthonormal bases (uᵢ) of E and (vⱼ) of F, ⟪x, T y⟫ = ∑ᵢ ∑ⱼ ⟪x, uᵢ⟫ ⟪uᵢ, T vⱼ⟫ ⟪vⱼ, y⟫ for every linear map T : F →ₗ[𝕜] E.

theorem Complex.isometryOfOrthonormal_symm_apply_eq_mk {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (b : OrthonormalBasis (Fin 2) ℝ V) (x : V) : (isometryOfOrthonormal b).symm x = { re := inner ℝ x (b 0), im := inner ℝ x (b 1) }

The complex coordinate of x given by Complex.isometryOfOrthonormal b is ⟪x, b₀⟫ + i ⟪x, b₁⟫.