Documentation

Lean 4 Proof

def cesGeneralHessianEntry (ρ F : ℝ)
    (P x : Fin J → ℝ) (i j : Fin J) : ℝ :=
  if i = j then
    F * (1 - ρ) * P i * (P i - 1) / (x i) ^ 2
  else
    F * (1 - ρ) * P i * P j / (x i * x j)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:55

Module Section

General CES Hessian at Arbitrary Allocation

In the same file