dot_affineShift
plain-language theorem explainer
The identity establishes linearity of the weighted dot product under componentwise affine shifts. Researchers formalizing the radical distribution of the rank-one log-coordinate Hessian cite it to verify that shifts along orthogonal directions preserve level sets. The proof expands the finite sum definition, distributes the scalar multiplication via congruence, and separates terms with sum additivity and factoring.
Claim. Let $n$ be a natural number, let $α, t, v : ℝ^n$, and let $s ∈ ℝ$. Then the weighted dot product satisfies $∑_{i=1}^n α_i (t_i + s v_i) = ∑_{i=1}^n α_i t_i + s ∑_{i=1}^n α_i v_i$.
background
The module formalizes the radical distribution of the rank-one log-coordinate Hessian, which detects only the active direction α and therefore has radical equal to the hyperplane orthogonal to α. Vectors are maps from Fin n to reals; the weighted dot product is the sum α_i x_i. Affine shift translates a base vector t by the scalar multiple s v componentwise. This identity is the algebraic engine behind the two downstream theorems that characterize directions preserving affine leaves {x | dot α x = c}.
proof idea
The tactic proof unfolds the definitions of dot and affineShift. It rewrites the sum by distributing multiplication inside each term, applies Finset.sum_congr with the ring tactic on the index set, then invokes Finset.sum_add_distrib together with Finset.mul_sum to factor the scalar s out of the second sum.
why it matters
The result is invoked directly by affineShift_mem_LevelSet (which shows radical directions remain inside a fixed level set) and by preserves_own_leaf_iff_mem_Radical (which characterizes the radical as exactly the directions that preserve every affine leaf). It therefore completes the local description of the radical distribution as the constant hyperplane orthogonal to α in the log-coordinate metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.