Documentation

Lean 4 Proof

theorem isoquant_umbilic (J : ℕ) (ρ c : ℝ) (v : Fin J → ℝ) :
    secondFundamentalFormQF J ρ c v =
    cesPrincipalCurvature J ρ c * vecNormSq J v := rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:204

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file