Self-Adjointness of a Symmetric Slot Action

This statement proves self-adjointness of the action of a symmetric matrix on one tensor slot.

Let $M$ be a real $n\times n$ matrix satisfying $M^\mathsf T=M$. For $s\in\operatorname{Fin}(r)$ and coordinate tensors $T,S:(\operatorname{Fin}(r)\to\operatorname{Fin}(n))\to\mathbb R$, one has

Here the inner product is the finite coordinate-tensor inner product and $M^{(s)}$ is actOn M s. The identity is used to move symmetric slot actions between factors in tensor estimates.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.CoordinateTensor. Shown in its original module context. Proof omitted.

theorem inner_actOn_left (M : Matrix (Fin n) (Fin n) ℝ) (hM : M.IsSymm) (s : Fin r)
    (T S : (Fin r → Fin n) → ℝ) : inner (actOn M s T) S = inner T (actOn M s S)

Module navigation

Module: Analysis/Tensor/SlotAction.

Previous: actOn_mul · Next: inner_actSum_actSum.

Source excerpt, lines 352–353 · Frozen source 408915f.