quadraticHessian_eq
plain-language theorem explainer
The quadratic form of the n-dimensional Hessian equals cosh of the weighted dot product of alpha and t times the square of the dot product of alpha and v. Analysts of the rank-one Hessian in the reciprocal cost model cite this reduction. The proof unfolds the quadratic form, applies the direction lemma for the Hessian action, and rearranges the finite sum via commutativity and the dot definition.
Claim. For vectors $α, t, v ∈ ℝ^n$, the quadratic form of the Hessian satisfies $Q(α, t, v) = cosh(α · t) (α · v)^2$, where the dot denotes the weighted inner product $∑_i α_i t_i$ and $Q$ is the Hessian applied to the vector.
background
The module develops Hessian formulas for the n-dimensional reciprocal cost. In log-coordinates this cost depends only on the single weighted aggregate given by the dot product of alpha and t, so the Hessian is rank one and factors through the outer product alpha tensor alpha. Vec denotes n-component real vectors as maps from Fin n to reals. The dot product is the weighted sum $∑ α_i t_i$ over the components. The upstream result applyHessian_eq_direction states that the Hessian action on any vector is always parallel to alpha, specifically the map i ↦ cosh(dot alpha t) * alpha_i * dot alpha v.
proof idea
The proof unfolds quadraticHessian and dot, then rewrites with applyHessian_eq_direction. A calc block factors cosh(dot alpha t) and dot alpha v out of the sum, recognizes the remaining sum as another dot product via sum_congr and ring, and finishes with algebraic simplification.
why it matters
This identity feeds quadraticHessian_nonneg (nonnegativity of the form) and quadraticHessian_eq_zero_iff (kernel characterization via the radical distribution). It supports the module claim that the n-dimensional cost depends only on one aggregate direction, yielding a rank-one Hessian. The result closes an algebraic step in the Cost.Ndim analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.