Documentation

Lean 4 Proof

theorem cesInner_symmetric {α ρ x : ℝ} (_hα : 0 < α) (_hα1 : α < 1) :
    cesInner α ρ x x = x ^ ρ := by
  simp only [cesInner]
  have : α + (1 - α) = 1 := by ring
  nlinarith

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:103

Module Section

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

In the same file