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_eq_sum_inv_gram: in an arbitrary basis, the metric trace contracts the form against the inverse Gram matrix of the basis.
• 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.

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.

theorem TauCeti.bilinFormTrace_eq_sum_inv_gram {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [FiniteDimensional ℝ W] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (B : LinearMap.BilinForm ℝ W) (b : Module.Basis ι ℝ W) : bilinFormTrace B = ∑ i : ι, ∑ j : ι, (Matrix.gram ℝ ⇑b)⁻¹ i j * (B (b i)) (b j)

In an arbitrary basis b, the metric trace contracts the form against the inverse Gram matrix of b: tr_g B = ∑ i j, (G⁻¹)ᵢⱼ B(bᵢ, bⱼ) with Gᵢⱼ = ⟪bᵢ, bⱼ⟫. This is the classical index formula gⁱʲ Bᵢⱼ; the basis need not be orthogonal.

@[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.