CES Third Deriv Value

def proved Foundations

Documentation

Lean 4 Proof

def cesThirdDerivValue (J : ℕ) (ρ c : ℝ) : ℝ :=
  curvatureK J ρ / (↑J ^ 2 * c ^ 2) * ((2 * ↑J - 1) - ρ * (↑J - 2))

Dependency Graph

Used by

ces_third_derivative_pos

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:22

Module Section

Further properties of CES curvature (Paper 1, Section 9):

In the same file

ces_third_derivative_pos asymmetryRatio asymmetry_exceeds_one knockoutRetained knockout_partial_retained knockout_total_failure knockout_no_failure criticalFailures dualExponent dualEigenvaluePerp curvature_conservation excessSavingCoeff substitution_savings