English
In a real inner product space E with an orthonormal basis v, the canonical covariant tensor equals the sum ∑ i v_i ⊗ v_i.
Русский
Для вещественного пространства с ортонормированным основанием v канонический ковариантный тензор равен сумме ∑ i v_i ⊗ v_i.
LaTeX
$$$\mathrm{canonicalCovariantTensor}(E) = \sum_i v_i \otimes v_i,$ где $v$ — ортонормированное базисное множество.$$
Lean4
/-- Representation of the canonical covariant tensor in terms of an orthonormal basis. -/
theorem canonicalCovariantTensor_eq_sum [FiniteDimensional ℝ E] {ι : Type*} [Fintype ι] (v : OrthonormalBasis ι ℝ E) :
InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) :=
by
let w := stdOrthonormalBasis ℝ E
calc
∑ m, w m ⊗ₜ[ℝ] w m
_ = ∑ m, ∑ n, ⟪w m, w n⟫_ℝ • w m ⊗ₜ[ℝ] w n := by
congr 1 with m
rw [Fintype.sum_eq_single m _, orthonormal_iff_ite.1 w.orthonormal]
· simp only [↓reduceIte, one_smul]
simp only [orthonormal_iff_ite.1 w.orthonormal, ite_smul, one_smul, zero_smul, ite_eq_right_iff]
tauto
_ = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪v i, w n⟫_ℝ) • w m ⊗ₜ[ℝ] w n := by
simp_rw [OrthonormalBasis.sum_inner_mul_inner v]
_ = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪w n, v i⟫_ℝ) • w m ⊗ₜ[ℝ] w n := by simp only [real_inner_comm (w _)]
_ = ∑ i, (∑ m, ⟪w m, v i⟫_ℝ • w m) ⊗ₜ[ℝ] ∑ n, ⟪w n, v i⟫_ℝ • w n :=
by
simp only [sum_tmul, tmul_sum, smul_tmul_smul, Finset.sum_comm (γ := ι), Finset.sum_smul]
rw [Finset.sum_comm]
_ = ∑ i, v i ⊗ₜ[ℝ] v i := by simp only [w.sum_repr' (v _)]
