Documentation

Lean 4 Proof

theorem goldenRule_cobbDouglas {α : ℝ} (_hα : 0 < α) (_hα1 : α < 1) :
    capitalShare α 0 1 1 = α :=
  capitalShare_cobbDouglas (by norm_num) (by norm_num)

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:220

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file