Documentation

Lean 4 Proof

theorem meanCurvature_pos (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) :
    0 < meanCurvatureTrace J ρ c := by
  simp only [meanCurvatureTrace]
  apply mul_pos
  · have : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
    linarith
  · exact curvature_pos hJ hρ hc

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:114

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file