Documentation

Lean 4 Proof

theorem curvature_lemma (_hJ : 2 ≤ J) {ρ : ℝ} (_hρ : ρ < 1)
    {c : ℝ} (_hc : 0 < c) :
    cesPrincipalCurvature J ρ c = (1 - ρ) / (c * Real.sqrt ↑J) := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/Hessian.lean:203

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file