Metric trace of a bilinear form

This file defines the metric trace of a bilinear form on a finite-dimensional real inner product space. The definition contracts the form against Mathlib's canonical covariant tensor, making it independent of any choice of basis.

Main definitions

• TauCeti.bilinFormTrace: the metric trace of a real bilinear form.

Main statements

• TauCeti.bilinFormTrace_eq_sum: in an orthonormal basis, the metric trace is the sum of the diagonal values.
• TauCeti.bilinFormTrace_inner: the metric trace of the inner product is the real dimension.

noncomputable def TauCeti.bilinFormTrace {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [FiniteDimensional ℝ W] : LinearMap.BilinForm ℝ W →ₗ[ℝ] ℝ

The metric trace of a bilinear form, obtained by contracting it against the canonical covariant tensor of the inner product.

Equations

• TauCeti.bilinFormTrace = LinearMap.applyₗ (InnerProductSpace.canonicalCovariantTensor W) ∘ₗ ↑(TensorProduct.lift.equiv (RingHom.id ℝ) W W ℝ)

theorem TauCeti.bilinFormTrace_apply {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [FiniteDimensional ℝ W] (B : LinearMap.BilinForm ℝ W) : bilinFormTrace B = (TensorProduct.lift B) (InnerProductSpace.canonicalCovariantTensor W)

The metric trace is evaluation on the canonical covariant tensor.

theorem TauCeti.bilinFormTrace_eq_sum {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [FiniteDimensional ℝ W] {i : Type u_2} [Fintype i] (B : LinearMap.BilinForm ℝ W) (b : OrthonormalBasis i ℝ W) : bilinFormTrace B = ∑ j : i, (B (b j)) (b j)

In an orthonormal basis, the metric trace is the sum of the diagonal values.

@[simp]

theorem TauCeti.bilinFormTrace_inner {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [FiniteDimensional ℝ W] : bilinFormTrace (innerₗ W) = ↑(Module.finrank ℝ W)

The metric trace of the inner product is the real dimension.