Documentation

Lean 4 Proof

theorem secondFF_from_hessian (hJ : 0 < J) (ρ c : ℝ) (hc : 0 < c)
    (v : Fin J → ℝ) (hv : orthToOne J v) :
    secondFundamentalFormQF J ρ c v =
    -cesHessianQF J ρ c v * Real.sqrt ↑J := by
  rw [cesHessianQF_on_perp hJ ρ c hc v hv]
  simp only [secondFundamentalFormQF]
  rw [curvature_eq_neg_eigenvalue_sqrt hJ ρ c hc]
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:97

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file