vec2
plain-language theorem explainer
vec2 supplies the two-component vector constructor for the positive-coordinate Hessian model. It is the standard way to form the weight vector and coordinate vector when specializing the n-dimensional aggregate to two dimensions. Researchers working on the 2x2 reciprocal cost cite it to instantiate the Vec 2 type in determinant and degeneracy statements. The declaration is a direct abbreviation that packages the Lean vector literal into the coordinate-function type.
Claim. The two-component vector is defined by $vec_2(u,v) := (u,v) : Fin 2 → ℝ$, the function sending index 0 to $u$ and index 1 to $v$.
background
The module develops explicit Hessian formulas for the multi-component reciprocal cost in positive coordinates. Vec n is the abbreviation for n-component real vectors realized as functions Fin n → ℝ. The aggregate function is the exponential aggregate R(x) = exp(∑ α_i log x_i), which serves as the scale parameter in every Hessian entry.
proof idea
This is a one-line abbreviation that directly constructs the two-element vector literal ![u, v] and returns it as an element of the Vec 2 type alias.
why it matters
vec2 is the foundational constructor used by every 2 × 2 result in the module, including det_xHessianMatrix2_formula, det_xHessianMatrix2_zero_cost, det_xHessianMatrix2_ne_zero_of_generic, xHessianMatrix2, and xHessianMatrix2_eq_general. It enables the explicit specialization of the general Hessian entry formula to two dimensions and supports the analysis of the reciprocal cost in the two-dimensional positive-coordinate setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.