theorem
proved
quadraticHessian_nonneg
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cost.Ndim.Hessian on GitHub at line 112.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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