Documentation

Lean 4 Proof

theorem curvature_alt_form (hJ : 2 ≤ J) (ρ c : ℝ) (hc : c ≠ 0) :
    cesPrincipalCurvature J ρ c =
    curvatureK J ρ * Real.sqrt ↑J / (c * (↑J - 1)) := by
  simp only [cesPrincipalCurvature, curvatureK]
  have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast (by omega : 0 < J)
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  have hJ1ne : (↑J : ℝ) - 1 ≠ 0 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
    linarith
  have hsqrt_ne : Real.sqrt ↑J ≠ 0 := by
    exact ne_of_gt (Real.sqrt_pos_of_pos hJpos)
  have hsqrt_sq : Real.sqrt ↑J * Real.sqrt ↑J = ↑J :=
    Real.mul_self_sqrt (le_of_lt hJpos)
  have hsqrt_sq' : Real.sqrt ↑J ^ 2 = ↑J := by
    rw [sq, hsqrt_sq]
  field_simp
  rw [hsqrt_sq']

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Hessian.lean:220

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file