Documentation

Lean 4 Proof

theorem chordalDistSq_nonneg (x y : Fin J → ℝ) (c : ℝ) :
    0 ≤ chordalDistSq J x y c := by
  simp only [chordalDistSq, isoquantDistSq]
  exact Finset.sum_nonneg fun j _ => sq_nonneg _

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:238

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file