Documentation

Lean 4 Proof

theorem gradientNormSq_pos (hJ : 0 < J) : 0 < gradientNormSq J := by
  simp only [gradientNormSq]
  exact div_pos one_pos (Nat.cast_pos.mpr hJ)

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:38

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file