Documentation

Lean 4 Proof

theorem positive_curvature_amplifies_gap (hJ : 2 ≤ J) {ρ₁ ρ₂ : ℝ}
    (_hρ₁ : ρ₁ < 1) (hρ₂ : ρ₂ < 1) (h12 : ρ₁ < ρ₂) {c : ℝ} (hc : 0 < c) :
    sectionalCurvature J ρ₂ c < sectionalCurvature J ρ₁ c := by
  simp only [sectionalCurvature, cesPrincipalCurvature, div_pow]
  apply div_lt_div_of_pos_right
  · -- (1-ρ₂)² < (1-ρ₁)²
    have h1 : 0 < 1 - ρ₂ := by linarith
    have h2 : 1 - ρ₂ < 1 - ρ₁ := by linarith
    nlinarith [sq_nonneg (1 - ρ₁ - (1 - ρ₂))]
  · -- (c * √J)² > 0
    positivity

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:294

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file