Composition of Matrix Actions on One Tensor Slot

This statement identifies the action of a matrix product on one slot of a coordinate tensor.

Let $n,r\in\mathbb N$, let $M,N$ be real $n\times n$ matrices, let $s\in\operatorname{Fin}(r)$, and let $T:(\operatorname{Fin}(r)\to\operatorname{Fin}(n))\to\mathbb R$. Then

where $A^{(s)}T$ denotes the Lean operation actOn A s T. This algebraic identity is used to manipulate slotwise matrix actions on coordinate tensors.

Original Lean declaration header

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

theorem actOn_mul (M N : Matrix (Fin n) (Fin n) ℝ) (s : Fin r) (T : (Fin r → Fin n) → ℝ) :
    actOn (M * N) s T = actOn M s (actOn N s T)

Module navigation

Module: Analysis/Tensor/SlotAction.

Previous: drift_expression_ge · Next: inner_actOn_left.

Source excerpt, lines 315–316 · Frozen source 408915f.