AApply_add
plain-language theorem explainer
The rank-one operator A defined componentwise by A(v)_i = λ (β♯)_i (β · v) is additive: A(v + w) = A v + A w. Workers on the finite-dimensional cost projector algebra cite this when building the quadratic relation A² = μ A and the normalized projector P. The proof evaluates pointwise, unfolds the definition to a scalar multiple of a dot product sum, then distributes the sum over vector addition via mul_add and ring arithmetic.
Claim. Let $A$ be the operator $A(v)_i = λ (β^♯)_i (β · v)$ where $β^♯$ is the vector obtained by raising the covector $β$ with the inverse kernel $h^{-1}$. Then $A(v + w) = A v + A w$.
background
Vec n denotes the space of real n-tuples written as functions Fin n → ℝ. The weighted inner product dot α t equals ∑_i α_i t_i. The map sharp hInv β raises the covector β to a vector via ∑_j hInv_i j β_j. AApply lam hInv β is the rank-one operator whose action on v is the vector whose i-th component is lam times (sharp hInv β)_i times (dot β v). The module develops the finite-dimensional operator algebra for the cost-induced projector, including the quadratic law A² = μ A and the normalized projector P.
proof idea
Apply funext to reduce to a pointwise equality at each index i. Unfold AApply and dot, then rewrite the sum ∑ β_j (v_j + w_j) as the sum of two separate dot products by invoking mul_add together with Finset.sum_add_distrib. The resulting expression factors into two copies of the AApply definition, which are reassembled by simp and ring.
why it matters
AApply_add supplies the additivity needed to extend the rank-one operator to the full projector algebra. It is invoked directly by AApply_sub and PApply_add, which in turn support the quadratic relation A² = μ A and the normalized projector P inside the cost-induced operator framework. The result closes a basic algebraic step in the finite-dimensional picture before passage to the continuous or infinite-dimensional setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.