Documentation

Lean 4 Proof

theorem sectionalCurvature_explicit (_hJ : 0 < J) {ρ c : ℝ} (_hc : c ≠ 0) :
    sectionalCurvature J ρ c = (1 - ρ) ^ 2 / (↑J * c ^ 2) := by
  simp only [sectionalCurvature, cesPrincipalCurvature]
  rw [div_pow, mul_pow, Real.sq_sqrt (Nat.cast_nonneg J)]
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:158

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file