Documentation

Lean 4 Proof

theorem principalCurvature_trichotomy (hJ : 2 ≤ J) {c : ℝ} (hc : 0 < c) (ρ : ℝ) :
    (ρ < 1 → 0 < cesPrincipalCurvature J ρ c) ∧
    (ρ = 1 → cesPrincipalCurvature J ρ c = 0) ∧
    (1 < ρ → cesPrincipalCurvature J ρ c < 0) := by
  refine ⟨fun hρ => curvature_pos hJ hρ hc, fun hρ => ?_, fun hρ => ?_⟩
  · simp [cesPrincipalCurvature, hρ]
  · simp only [cesPrincipalCurvature]
    apply div_neg_of_neg_of_pos
    · linarith
    · apply mul_pos hc
      exact Real.sqrt_pos_of_pos (Nat.cast_pos.mpr (by omega))

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:183

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file