AApply
plain-language theorem explainer
AApply encodes the coordinate action of the rank-one operator A = λ β♯ ⊗ β on vectors in R^n. Researchers building the finite-dimensional cost algebra cite it when deriving linearity and the quadratic law A² = μ A. The body is a direct lambda that raises β via sharp and scales each output component by the scalar dot product β · v.
Claim. The map $A: V_n → V_n$ is given componentwise by $(A v)_i = λ · (♯_{h^{-1}} β)_i · (β · v)$, where $V_n = ℝ^n$ with coordinates indexed by Fin n, ♯ raises the covector β using the inverse kernel $h^{-1}$, and · denotes the weighted dot product.
background
The Cost.Ndim.Projector module assembles the operator algebra for rank-one tensors arising from a covector β and inverse metric kernel hInv. Vec n is the type of n-component real vectors realized as functions Fin n → ℝ. The sharp map raises β to a vector by the summation ∑_j hInv i j · β j, while dot computes the weighted inner product ∑_i α i · t i.
proof idea
The definition is realized directly by the term fun v => fun i => lam * sharp hInv β i * dot β v. It composes the upstream sharp operation to obtain the raised vector and multiplies by the scalar produced by the upstream dot product.
why it matters
AApply supplies the concrete operator whose properties are proved in the sibling theorems AApply_add, AApply_smul, AApply_sq and dot_AApply. Those results establish the quadratic relation A² = μ A that feeds the normalized projector P. The construction sits inside the rank-one tensor picture of the module documentation and supports the almost-product operators used in the Recognition Science cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.