Documentation

Lean 4 Proof

def cesHessianEntry (J : ℕ) (ρ c : ℝ) (i j : Fin J) : ℝ :=
  (1 - ρ) / ((↑J : ℝ) ^ 2 * c) * (1 - if i = j then ↑J else 0)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Hessian.lean:127

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file