Documentation

Lean 4 Proof

theorem sectionalCurvature_from_K (hJ : 2 ≤ J) (ρ c : ℝ) (hc : c ≠ 0) :
    sectionalCurvature J ρ c =
    curvatureK J ρ ^ 2 * ↑J / (c ^ 2 * (↑J - 1) ^ 2) := by
  simp only [sectionalCurvature]
  rw [curvature_alt_form hJ ρ c hc, div_pow, mul_pow,
      Real.sq_sqrt (Nat.cast_nonneg J)]
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:167

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file