PApply_smul
plain-language theorem explainer
The normalized projector PApply commutes with scalar multiplication on its input vector. Researchers developing the finite-dimensional cost operators cite this linearity when scaling inputs in projector identities. The proof is a one-line wrapper reducing via the definition of PApply to the scalar-multiplication property of AApply.
Claim. Let $P$ be the normalized projector $P(v) = mu^{-1} A(v)$ associated to parameters $lam$, inverse kernel $hInv$, and covector $beta$. Then for any real scalar $c$ and vector $v$, $P(c v) = c P(v)$.
background
The module packages the finite-dimensional operator algebra behind the rank-one tensor picture. A covector $beta$ and inverse metric kernel $hInv$ determine an operator $A$, its quadratic law $A^2 = mu A$, and the normalized projector $P = mu^{-1} A$. Vec $n$ denotes the type of $n$-component real vectors as coordinate functions. The upstream theorem AApply_smul establishes the identical scalar-multiplication identity for the un-normalized operator AApply.
proof idea
One-line wrapper that applies function extensionality followed by simplification, unfolding the definition of PApply and invoking AApply_smul together with associativity and commutativity of multiplication.
why it matters
This linearity supports the almost-product operator FApply and its interactions with PApply, feeding directly into the downstream results FApply_smul, PApply_FApply, and PApply_neg. It completes a basic algebraic property of the cost-induced projector within the module's development of the rank-one tensor picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.