applyHessian_of_dot_zero

formal source

  81          simp [dot, mul_comm, mul_assoc]
  82
  83/-- Vectors orthogonal to `α` lie in the kernel of the Hessian. -/
  84theorem applyHessian_of_dot_zero {n : ℕ} (α t v : Vec n)
  85    (hv : dot α v = 0) :
  86    applyHessian α t v = 0 := by
  87  funext i
  88  simp [applyHessian_eq_direction, hv]
  89
  90/-- The Hessian quadratic form depends only on the single active direction `dot α v`. -/
  91theorem quadraticHessian_eq {n : ℕ} (α t v : Vec n) :
  92    quadraticHessian α t v = Real.cosh (dot α t) * (dot α v) ^ 2 := by
  93  unfold quadraticHessian dot
  94  rw [applyHessian_eq_direction]
  95  calc
  96    ∑ i : Fin n, v i * (Real.cosh (dot α t) * α i * dot α v)
  97        = ∑ i : Fin n, Real.cosh (dot α t) * dot α v * (v i * α i) := by
  98            apply Finset.sum_congr rfl
  99            intro i hi
 100            ring
 101    _ = (Real.cosh (dot α t) * dot α v) * ∑ i : Fin n, v i * α i := by
 102          rw [Finset.mul_sum]
 103    _ = Real.cosh (dot α t) * (dot α v) * dot α v := by
 104          congr 1
 105          unfold dot
 106          apply Finset.sum_congr rfl
 107          intro i hi
 108          ring
 109    _ = Real.cosh (dot α t) * (dot α v) ^ 2 := by
 110          ring
 111
 112theorem quadraticHessian_nonneg {n : ℕ} (α t v : Vec n) :
 113    0 ≤ quadraticHessian α t v := by
 114  rw [quadraticHessian_eq]