Documentation

Lean 4 Proof

theorem curvatureK_two_factor_pos {ρ : ℝ} (hρ : ρ < 1) :
    0 < curvatureK 2 ρ := by
  rw [curvatureK_two_factor]
  linarith

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:343

Module Section

Two-Factor CES Production Function (Layer 1 of Macro Extension)

In the same file