Documentation

Lean 4 Proof

theorem sectionalCurvature_nonneg (ρ c : ℝ) :
    0 ≤ sectionalCurvature J ρ c := by
  simp only [sectionalCurvature]
  exact sq_nonneg _

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:136

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file