Documentation

Lean 4 Proof

theorem sectionalCurvature_via_bridge {J : ℕ} {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : c ≠ 0) (hJ : (↑J : ℝ) ≠ 0) :
    sectionalCurvature J ρ c =
    ↑J * c ^ 2 * bridgeRatio ρ ^ 2 * escortFisherEigenvalue J ρ c ^ 2 := by
  simp only [sectionalCurvature, cesPrincipalCurvature, bridgeRatio,
             escortFisherEigenvalue]
  rw [div_pow, mul_pow, Real.sq_sqrt (Nat.cast_nonneg J)]
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:256

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file