Sections / Section 5: General Hessian and Isoquant Geometry / ces_gradient_symmetric

CES Gradient Symmetric

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem ces_gradient_symmetric (_hJ : 0 < J) (_ρ : ℝ) (_c : ℝ) (_hc : 0 < c)
    (_j : Fin J) :
    (1 : ℝ) / ↑J = 1 / ↑J := by rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/Hessian.lean:55

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file

cesHessianQF cesEigenvaluePerp vecSum orthToOne vecNormSq cesHessianQF_on_one cesHessianQF_on_perp cesHessianQF_neg_semidef ces_strict_concavity_on_perp cesHessianEntry cesHessianQF_eq_sum cesPrincipalCurvature curvature_lemma curvature_pos curvature_alt_form