Documentation

Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Canonical tensors in real inner product spaces #

Given an InnerProductSpace ℝ E, this file defines two canonical tensors.

The theorem canonicalCovariantTensor_eq_sum shows that InnerProductSpace.canonicalCovariantTensor E can be computed from any orthonormal basis v as ∑ i, (v i) ⊗ₜ[ℝ] (v i).

The canonical contravariant tensor corresponding to the inner product

Equations
Instances For

    The canonical covariant tensor corresponding to InnerProductSpace.canonicalContravariantTensor under the identification of E with its dual.

    Equations
    Instances For

      Representation of the canonical covariant tensor in terms of an orthonormal basis.