Documentation

Lean 4 Proof

private theorem curvature_eq_neg_eigenvalue_sqrt (hJ : 0 < J) (ρ c : ℝ) (hc : 0 < c) :
    cesPrincipalCurvature J ρ c = -cesEigenvaluePerp J ρ c * Real.sqrt ↑J := by
  simp only [cesPrincipalCurvature, cesEigenvaluePerp]
  have hJpos : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hcne : c ≠ 0 := ne_of_gt hc
  have hsqrt_ne : Real.sqrt ↑J ≠ 0 := ne_of_gt (Real.sqrt_pos_of_pos hJpos)
  have hsqrt_sq : Real.sqrt ↑J * Real.sqrt ↑J = ↑J := Real.mul_self_sqrt hJpos.le
  field_simp
  rw [sq, hsqrt_sq]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:84

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file