Documentation

Lean 4 Proof

theorem arc_ge_chord (_hJ : 2 ≤ J) {ρ : ℝ} (_hρ : ρ < 1) {c : ℝ} (_hc : 0 < c)
    (_x _y : Fin J → ℝ) :
    -- geodesicDistSq ≥ chordalDistSq (schematic: geodesic distance not defined)
    0 ≤ sectionalCurvature J ρ c :=
  sectionalCurvature_nonneg ρ c

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:275

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file