Documentation

Lean 4 Proof

def chordalDistSq (J : ℕ) (x y : Fin J → ℝ) (c : ℝ) : ℝ :=
  isoquantDistSq J x y c c

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:234

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file