Documentation

Lean 4 Proof

theorem curvature_pos (_hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) :
    0 < cesPrincipalCurvature J ρ c := by
  simp only [cesPrincipalCurvature]
  apply div_pos
  · linarith
  · apply mul_pos hc
    apply Real.sqrt_pos_of_pos
    exact_mod_cast (by omega : 0 < J)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Hessian.lean:209

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file