quadraticHessian_eq

formal source

  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]
 115  positivity
 116
 117end Ndim
 118end Cost
 119end IndisputableMonolith