Documentation

Lean 4 Proof

def meanCurvatureTrace (J : ℕ) (ρ c : ℝ) : ℝ :=
  (↑J - 1) * cesPrincipalCurvature J ρ c

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:78

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file