Documentation

Lean 4 Proof

theorem sectionalCurvature_eq_zero_iff (hJ : 0 < J) {ρ c : ℝ} (hc : 0 < c) :
    sectionalCurvature J ρ c = 0 ↔ ρ = 1 := by
  simp only [sectionalCurvature, cesPrincipalCurvature]
  have hJpos : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hdenom : c * Real.sqrt ↑J ≠ 0 :=
    mul_ne_zero hc.ne' (ne_of_gt (Real.sqrt_pos_of_pos hJpos))
  rw [sq_eq_zero_iff, div_eq_zero_iff]
  constructor
  · rintro (h | h)
    · linarith
    · exact absurd h hdenom
  · intro h; left; linarith

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:144

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file