Documentation

Lean 4 Proof

theorem curvatureK_two_factor (ρ : ℝ) :
    curvatureK 2 ρ = (1 - ρ) / 2 := by
  simp only [curvatureK]
  push_cast
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:336

Module Section

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

In the same file